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

Theorem nfima 5123
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  |-  F/_ x A
nfima.2  |-  F/_ x B
Assertion
Ref Expression
nfima  |-  F/_ x
( A " B
)

Proof of Theorem nfima
StepHypRef Expression
1 df-ima 4805 . 2  |-  ( A
" B )  =  ran  ( A  |`  B )
2 nfima.1 . . . 4  |-  F/_ x A
3 nfima.2 . . . 4  |-  F/_ x B
42, 3nfres 5060 . . 3  |-  F/_ x
( A  |`  B )
54nfrn 5024 . 2  |-  F/_ x ran  ( A  |`  B )
61, 5nfcxfr 2499 1  |-  F/_ x
( A " B
)
Colors of variables: wff set class
Syntax hints:   F/_wnfc 2489   ran crn 4793    |` cres 4794   "cima 4795
This theorem is referenced by:  nfimad  5124  csbima12g  5125  nfsup  7349  nfoi  7376  nfseq  11220  gsum2d2  15435  ptbasfi  17493  mbfposr  19222  itg1climres  19284  limciun  19459  funimass4f  23568  aomclem8  26750  rfcnpre1  27281  rfcnpre2  27293
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-rab 2637  df-v 2875  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-nul 3544  df-if 3655  df-sn 3735  df-pr 3736  df-op 3738  df-br 4126  df-opab 4180  df-xp 4798  df-cnv 4800  df-dm 4802  df-rn 4803  df-res 4804  df-ima 4805
  Copyright terms: Public domain W3C validator