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

Theorem nffv 6660
 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 𝑥𝐹
nffv.2 𝑥𝐴
Assertion
Ref Expression
nffv 𝑥(𝐹𝐴)

Proof of Theorem nffv
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 df-fv 6335 . 2 (𝐹𝐴) = (℩𝑦𝐴𝐹𝑦)
2 nffv.2 . . . 4 𝑥𝐴
3 nffv.1 . . . 4 𝑥𝐹
4 nfcv 2955 . . . 4 𝑥𝑦
52, 3, 4nfbr 5078 . . 3 𝑥 𝐴𝐹𝑦
65nfiotaw 6290 . 2 𝑥(℩𝑦𝐴𝐹𝑦)
71, 6nfcxfr 2953 1 𝑥(𝐹𝐴)
 Colors of variables: wff setvar class Syntax hints:  Ⅎwnfc 2936   class class class wbr 5031  ℩cio 6284  ‘cfv 6327 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5032  df-iota 6286  df-fv 6335 This theorem is referenced by:  nffvmpt1  6661  nffvd  6662  fvelimad  6712  dffn5f  6716  fvmptss  6762  fvmptex  6764  fvmptf  6771  fvmptnf  6772  eqfnfv2f  6788  ralrnmptw  6842  ralrnmpt  6844  ffnfvf  6865  funiunfvf  6991  dff13f  6997  nfiso  7059  nfwrecs  7939  nfrdg  8040  rdgsucmptf  8054  rdgsucmptnf  8055  frsucmpt  8063  frsucmptn  8064  rankidb  9220  rankval4  9287  dfac8clem  9450  cardaleph  9507  hsmexlem2  9845  axcc2  9855  uniimadomf  9963  nfseq  13381  seqof2  13431  rlim2  14852  nfsum1  15045  nfsum  15046  nfsumOLD  15047  sumeq2ii  15049  fsumrelem  15161  o1fsum  15167  nfcprod1  15263  nfcprod  15264  fprodefsum  15447  prdsbas3  16753  prdsdsval2  16756  yonedalem4b  17525  gsum2d2lem  19094  coe1fzgsumdlem  20944  evl1gsumdlem  20994  ptcldmpt  22233  ptcnp  22241  cnmpt11  22282  cnmpt21  22290  cnmptk2  22305  prdsdsf  22988  prdsxmet  22990  ovolfiniun  24119  ovoliunlem3  24122  ovoliun  24123  ovoliun2  24124  ovoliunnul  24125  volfiniun  24165  voliun  24172  mbfsup  24282  mbflim  24286  itg2splitlem  24366  itg2split  24367  itg2cnlem1  24379  isibl2  24384  nfitg1  24391  nfitg  24392  cbvitg  24393  itgabs  24452  dvlipcn  24611  lhop2  24632  dvfsumabs  24640  dvfsumrlim  24648  itgparts  24664  itgsubstlem  24665  ulmss  25006  itgulm2  25018  lgamgulmlem2  25629  lgamgulmlem6  25633  lgamgulm2  25635  lgseisenlem2  25974  dchrisumlem3  26089  cnlnadjlem5  29868  dfimafnf  30409  2ndresdju  30425  esumfzf  31474  voliune  31634  volfiniune  31635  bnj1534  32271  bnj1542  32275  bnj958  32358  bnj1000  32359  bnj1446  32463  bnj1447  32464  bnj1448  32465  bnj1466  32471  bnj1467  32472  bnj1519  32483  bnj1520  32484  bnj1529  32488  cvmcov  32659  trpredlem1  33215  trpredrec  33226  sltval2  33312  rdgssun  34835  exrecfnlem  34836  finxpreclem2  34847  finxpreclem6  34853  poimirlem23  35120  poimirlem27  35124  itgabsnc  35166  riotaocN  36545  cdleme32d  37780  cdleme32f  37782  ltrniotaval  37917  cdlemksv2  38183  cdlemkuv2  38203  cdlemk36  38249  cdlemk38  38251  cdlemk19x  38279  cdlemk11t  38282  mzpsubst  39753  aomclem8  40069  mnringmulrcld  41000  binomcxplemdvbinom  41121  binomcxplemdvsum  41123  binomcxplemnotnn0  41124  evth2f  41708  fvelrnbf  41711  evthf  41720  rfcnpre3  41726  rfcnpre4  41727  rfcnnnub  41729  refsum2cnlem1  41730  dffo3f  41869  allbutfiinf  42118  monoordxr  42183  monoord2xr  42185  fmul01  42283  fmuldfeqlem1  42285  fmuldfeq  42286  fmul01lt1lem1  42287  fmul01lt1lem2  42288  fmul01lt1  42289  cncfmptss  42290  mulc1cncfg  42292  expcnfg  42294  fprodabs2  42298  climmulf  42307  climexp  42308  climsuse  42311  climrecf  42312  climinff  42314  climaddf  42318  mullimc  42319  idlimc  42329  limcperiod  42331  neglimc  42350  addlimc  42351  0ellimcdiv  42352  fnlimfv  42366  climreclf  42367  fnlimcnv  42370  fnlimfvre  42377  fnlimfvre2  42380  fnlimf  42381  fnlimabslt  42382  climfveqf  42383  climmptf  42384  climeldmeqf  42386  limsupref  42388  limsupbnd1f  42389  climbddf  42390  climeqf  42391  limsuppnfd  42405  climinf2  42410  limsuppnf  42414  limsupubuz  42416  climinfmpt  42418  limsupmnf  42424  limsupequz  42426  limsupre2  42428  limsupmnfuz  42430  limsupre3  42436  limsupre3uz  42439  limsupreuz  42440  climuz  42447  lmbr3  42450  limsupgt  42481  liminfvalxr  42486  liminfreuz  42506  liminflt  42508  xlimpnfxnegmnf  42517  liminfpnfuz  42519  xlimmnf  42544  xlimpnf  42545  dfxlim2  42551  xlimpnfxnegmnf2  42561  cncfshift  42577  icccncfext  42590  cncficcgt0  42591  cncfiooicclem1  42596  dvnmul  42646  dvnprodlem1  42649  itgsubsticclem  42678  stoweidlem3  42706  stoweidlem23  42726  stoweidlem26  42729  stoweidlem28  42731  stoweidlem29  42732  stoweidlem31  42734  stoweidlem34  42737  stoweidlem36  42739  stoweidlem42  42745  stoweidlem48  42751  stoweidlem51  42754  stoweidlem52  42755  stoweidlem59  42762  wallispilem5  42772  stirlinglem4  42780  stirlinglem11  42787  stirlinglem12  42788  stirlinglem13  42789  stirlinglem14  42790  stirlinglem15  42791  fourierdlem20  42830  fourierdlem31  42841  fourierdlem79  42888  fourierdlem89  42898  fourierdlem91  42900  fourierdlem112  42921  fourierdlem115  42924  fourierd  42925  fourierclimd  42926  etransclem2  42939  etransclem48  42985  sge0revalmpt  43078  sge0fsummpt  43090  sge0iunmptlemfi  43113  sge0iunmptlemre  43115  sge0iunmpt  43118  sge0xadd  43135  sge0fsummptf  43136  sge0gtfsumgt  43143  iundjiun  43160  meadjiun  43166  voliunsge0lem  43172  meaiunincf  43183  meaiuninc3  43185  omeiunle  43217  omeiunltfirp  43219  ovncvrrp  43264  vonioo  43382  vonicc  43385  vonn0ioo2  43390  vonn0icc2  43392  pimltmnf2  43397  pimgtpnf2  43403  pimltpnf2  43409  pimgtmnf2  43410  pimdecfgtioc  43411  issmff  43429  smfpimltxrmpt  43453  smfpreimagtf  43462  smflim  43471  smfpimgtxr  43474  smfpimgtxrmpt  43478  smfmullem4  43487  smflim2  43498  smfpimcclem  43499  smfpimcc  43500  smfsup  43506  smfsupmpt  43507  smfsupxr  43508  smfinflem  43509  smfinf  43510  smfinfmpt  43511  smflimsuplem2  43513  smflimsuplem5  43516  smflimsuplem7  43518  smflimsup  43520  smfliminf  43523  nfafv  43753  nfsetrecs  45275  setrec2fun  45281
 Copyright terms: Public domain W3C validator