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

Theorem nffv 5493
Description: Bound-variable hypothesis builder for function value. (Contributed by NM, 14-Nov-1995.) (Revised by Mario Carneiro, 15-Oct-2016.)
Hypotheses
Ref Expression
nffv.1  |-  F/_ x F
nffv.2  |-  F/_ x A
Assertion
Ref Expression
nffv  |-  F/_ x
( F `  A
)
Dummy variable  y is distinct from all other variables.

Proof of Theorem nffv
StepHypRef Expression
1 df-fv 5230 . 2  |-  ( F `
 A )  = 
U. { y  |  ( F " { A } )  =  {
y } }
2 nffv.1 . . . . . 6  |-  F/_ x F
3 nffv.2 . . . . . . 7  |-  F/_ x A
43nfsn 3693 . . . . . 6  |-  F/_ x { A }
52, 4nfima 5020 . . . . 5  |-  F/_ x
( F " { A } )
65nfeq1 2430 . . . 4  |-  F/ x
( F " { A } )  =  {
y }
76nfab 2425 . . 3  |-  F/_ x { y  |  ( F " { A } )  =  {
y } }
87nfuni 3835 . 2  |-  F/_ x U. { y  |  ( F " { A } )  =  {
y } }
91, 8nfcxfr 2418 1  |-  F/_ x
( F `  A
)
Colors of variables: wff set class
Syntax hints:    = wceq 1624   {cab 2271   F/_wnfc 2408   {csn 3642   U.cuni 3829   "cima 4692   ` cfv 5222
This theorem is referenced by:  nffvmpt1  5494  nffvd  5495  dffn5f  5539  fvmptss  5571  fvmptex  5572  fvmptt  5577  fvmptf  5578  fvmptnf  5579  eqfnfv2f  5588  ralrnmpt  5631  ffnfvf  5648  fmptco  5653  funiunfvf  5737  dff13f  5746  nfiso  5783  offval2  6057  ofrfval2  6058  opabiota  6287  nfriota1  6308  nfrecs  6386  nfrdg  6423  rdgsucmptf  6437  rdgsucmptnf  6438  frsucmpt  6446  frsucmptn  6447  mptelixpg  6849  dom2lem  6897  rankidb  7468  rankval4  7535  dfac8clem  7655  acni2  7669  cardaleph  7712  hsmexlem2  8049  axcc2  8059  axdclem  8142  uniimadomf  8163  nfseq  11051  rlim2  11965  ello1mpt  11990  o1compt  12056  nfsum1  12158  nfsum  12159  sumfc  12177  zsum  12186  fsum  12188  fsumf1o  12191  sumss  12192  fsumcvg2  12195  fsumadd  12206  isummulc2  12220  fsummulc2  12241  fsumrelem  12260  o1fsum  12266  isumshft  12293  iserodd  12883  prdsbas3  13375  prdsdsval2  13378  yonedalem4b  14045  gsum2d2lem  15219  dprdwd  15241  gsumdixp  15387  evlslem4  16240  elptr2  17264  ptunimpt  17285  ptcldmpt  17303  ptclsg  17304  txcnp  17309  ptcnplem  17310  ptcnp  17311  cnmpt11  17352  cnmpt1t  17354  cnmpt21  17360  cnmptk2  17375  flfcnp2  17697  prdsdsf  17926  prdsxmet  17928  ovolfiniun  18855  ovoliunlem3  18858  ovoliun  18859  ovoliun2  18860  ovoliunnul  18861  volfiniun  18899  voliun  18906  mbfeqalem  18992  mbfpos  19001  mbfposb  19003  mbfsup  19014  mbfinf  19015  mbflim  19018  i1fposd  19057  itg2splitlem  19098  itg2split  19099  itg2cnlem1  19111  isibl2  19116  nfitg1  19123  nfitg  19124  cbvitg  19125  itgmpt  19132  itgeqa  19163  itgabs  19184  itggt0  19191  itgcn  19192  dvlipcn  19336  lhop2  19357  dvfsumabs  19365  dvfsumrlim  19373  itgparts  19389  itgsubstlem  19390  itgsubst  19391  elplyd  19579  coeeq2  19619  dgrle  19620  ulmss  19769  itgulm2  19780  leibpi  20233  rlimcnp  20255  o1cxp  20264  lgseisenlem2  20584  dchrisumlem3  20635  cnlnadjlem5  22644  dfimafnf  23035  cvmcov  23199  trpredlem1  23632  trpredrec  23643  sltval2  23711  axfelem5  23752  prodeq3ii  24708  nfprod1  24710  nfprod  24711  prodeqfv  24718  fprodserf  24721  fprodadd  24752  fprodneg  24778  fprodsub  24779  intopcoaconb  24940  elrfirn2  26171  mzpsubst  26226  eq0rabdioph  26256  monotoddzz  26428  aomclem8  26559  evth2f  27086  fvelrnbf  27089  evthf  27098  rfcnpre3  27104  rfcnpre4  27105  rfcnnnub  27107  refsum2cnlem1  27108  fmul01  27110  fmuldfeqlem1  27112  fmuldfeq  27113  fmul01lt1lem1  27114  fmul01lt1lem2  27115  fmul01lt1  27116  cncfmptss  27117  mulc1cncfg  27121  expcnfg  27126  climmulf  27130  climexp  27131  climsuse  27134  climrecf  27135  climinff  27137  stoweidlem3  27152  stoweidlem23  27172  stoweidlem26  27175  stoweidlem28  27177  stoweidlem29  27178  stoweidlem31  27180  stoweidlem34  27183  stoweidlem36  27185  stoweidlem42  27191  stoweidlem48  27197  stoweidlem51  27200  stoweidlem52  27201  stoweidlem59  27208  wallispilem5  27218  stirlinglem4  27226  stirlinglem11  27233  stirlinglem12  27234  stirlinglem13  27235  stirlinglem14  27236  stirlinglem15  27237  nfafv  27379  bnj1534  28153  bnj1542  28157  bnj958  28240  bnj1000  28241  bnj1446  28343  bnj1447  28344  bnj1448  28345  bnj1466  28351  bnj1467  28352  bnj1519  28363  bnj1520  28364  bnj1529  28368  riotaocN  28667  cdleme32d  29901  cdleme32f  29903  ltrniotaval  30038  cdlemksv2  30304  cdlemkuv2  30324  cdlemk36  30370  cdlemk38  30372  cdlemk19x  30400  cdlemk11t  30403
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 938  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-uni 3830  df-br 4026  df-opab 4080  df-xp 4695  df-cnv 4697  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-fv 5230
  Copyright terms: Public domain W3C validator