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

Theorem nfima 5930
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 5561 . 2 (𝐴𝐵) = ran (𝐴𝐵)
2 nfima.1 . . . 4 𝑥𝐴
3 nfima.2 . . . 4 𝑥𝐵
42, 3nfres 5848 . . 3 𝑥(𝐴𝐵)
54nfrn 5817 . 2 𝑥ran (𝐴𝐵)
61, 5nfcxfr 2973 1 𝑥(𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wnfc 2959  ran crn 5549  cres 5550  cima 5551
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-br 5058  df-opab 5120  df-xp 5554  df-cnv 5556  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561
This theorem is referenced by:  nfimad  5931  csbima12  5940  nfpred  6146  nfsup  8907  nfoi  8970  nfseq  13371  gsum2d2  19086  ptbasfi  22181  mbfposr  24245  itg1climres  24307  limciun  24484  funimass4f  30374  poimirlem16  34900  poimirlem19  34903  aomclem8  39651  areaquad  39813  nfcoll  40582  binomcxplemdvbinom  40675  binomcxplemdvsum  40677  binomcxplemnotnn0  40678  rfcnpre1  41266  rfcnpre2  41278  smfpimcc  43072
  Copyright terms: Public domain W3C validator