MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfima Structured version   Visualization version   GIF version

Theorem nfima 5632
Description: Bound-variable hypothesis builder for image. (Contributed by NM, 30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
Hypotheses
Ref Expression
nfima.1 𝑥𝐴
nfima.2 𝑥𝐵
Assertion
Ref Expression
nfima 𝑥(𝐴𝐵)

Proof of Theorem nfima
StepHypRef Expression
1 df-ima 5279 . 2 (𝐴𝐵) = ran (𝐴𝐵)
2 nfima.1 . . . 4 𝑥𝐴
3 nfima.2 . . . 4 𝑥𝐵
42, 3nfres 5553 . . 3 𝑥(𝐴𝐵)
54nfrn 5523 . 2 𝑥ran (𝐴𝐵)
61, 5nfcxfr 2900 1 𝑥(𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wnfc 2889  ran crn 5267  cres 5268  cima 5269
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-br 4805  df-opab 4865  df-xp 5272  df-cnv 5274  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279
This theorem is referenced by:  nfimad  5633  csbima12  5641  nfpred  5846  nfsup  8524  nfoi  8586  nfseq  13025  gsum2d2  18593  ptbasfi  21606  mbfposr  23638  itg1climres  23700  limciun  23877  funimass4f  29767  poimirlem16  33756  poimirlem19  33759  aomclem8  38151  areaquad  38322  binomcxplemdvbinom  39072  binomcxplemdvsum  39074  binomcxplemnotnn0  39075  rfcnpre1  39695  rfcnpre2  39707  smfpimcc  41538
  Copyright terms: Public domain W3C validator