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

Theorem nffv 6165
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 5865 . 2 (𝐹𝐴) = (℩𝑦𝐴𝐹𝑦)
2 nffv.2 . . . 4 𝑥𝐴
3 nffv.1 . . . 4 𝑥𝐹
4 nfcv 2761 . . . 4 𝑥𝑦
52, 3, 4nfbr 4669 . . 3 𝑥 𝐴𝐹𝑦
65nfiota 5824 . 2 𝑥(℩𝑦𝐴𝐹𝑦)
71, 6nfcxfr 2759 1 𝑥(𝐹𝐴)
Colors of variables: wff setvar class
Syntax hints:  wnfc 2748   class class class wbr 4623  cio 5818  cfv 5857
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2913  df-rex 2914  df-rab 2917  df-v 3192  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-op 4162  df-uni 4410  df-br 4624  df-iota 5820  df-fv 5865
This theorem is referenced by:  nffvmpt1  6166  nffvd  6167  dffn5f  6219  fvmptss  6259  fvmptex  6261  fvmptf  6267  fvmptnf  6268  eqfnfv2f  6281  ralrnmpt  6334  ffnfvf  6355  funiunfvf  6472  dff13f  6478  nfiso  6537  nfwrecs  7369  nfrdg  7470  rdgsucmptf  7484  rdgsucmptnf  7485  frsucmpt  7493  frsucmptn  7494  rankidb  8623  rankval4  8690  dfac8clem  8815  cardaleph  8872  hsmexlem2  9209  axcc2  9219  uniimadomf  9327  nfseq  12767  seqof2  12815  rlim2  14177  nfsum1  14370  nfsum  14371  sumeq2ii  14373  fsumrelem  14485  o1fsum  14491  nfcprod1  14584  nfcprod  14585  fprodefsum  14769  prdsbas3  16081  prdsdsval2  16084  yonedalem4b  16856  gsum2d2lem  18312  coe1fzgsumdlem  19611  evl1gsumdlem  19660  ptcldmpt  21357  ptcnp  21365  cnmpt11  21406  cnmpt21  21414  cnmptk2  21429  prdsdsf  22112  prdsxmet  22114  ovolfiniun  23209  ovoliunlem3  23212  ovoliun  23213  ovoliun2  23214  ovoliunnul  23215  volfiniun  23255  voliun  23262  mbfsup  23371  mbflim  23375  itg2splitlem  23455  itg2split  23456  itg2cnlem1  23468  isibl2  23473  nfitg1  23480  nfitg  23481  cbvitg  23482  itgabs  23541  dvlipcn  23695  lhop2  23716  dvfsumabs  23724  dvfsumrlim  23732  itgparts  23748  itgsubstlem  23749  ulmss  24089  itgulm2  24101  lgamgulmlem2  24690  lgamgulmlem6  24694  lgamgulm2  24696  lgseisenlem2  25035  dchrisumlem3  25114  cnlnadjlem5  28818  dfimafnf  29320  esumfzf  29954  voliune  30115  volfiniune  30116  bnj1534  30684  bnj1542  30688  bnj958  30771  bnj1000  30772  bnj1446  30874  bnj1447  30875  bnj1448  30876  bnj1466  30882  bnj1467  30883  bnj1519  30894  bnj1520  30895  bnj1529  30899  cvmcov  31006  trpredlem1  31481  trpredrec  31492  sltval2  31563  nobndlem5  31612  finxpreclem2  32898  finxpreclem6  32904  poimirlem23  33103  poimirlem27  33107  itgabsnc  33150  riotaocN  34015  cdleme32d  35251  cdleme32f  35253  ltrniotaval  35388  cdlemksv2  35654  cdlemkuv2  35674  cdlemk36  35720  cdlemk38  35722  cdlemk19x  35750  cdlemk11t  35753  mzpsubst  36830  aomclem8  37150  binomcxplemdvbinom  38073  binomcxplemdvsum  38075  binomcxplemnotnn0  38076  evth2f  38696  fvelrnbf  38699  evthf  38708  rfcnpre3  38714  rfcnpre4  38715  rfcnnnub  38717  refsum2cnlem1  38718  dffo3f  38873  fvelimad  38968  allbutfiinf  39146  fmul01  39248  fmuldfeqlem1  39250  fmuldfeq  39251  fmul01lt1lem1  39252  fmul01lt1lem2  39253  fmul01lt1  39254  cncfmptss  39255  mulc1cncfg  39257  expcnfg  39259  fprodabs2  39263  climmulf  39272  climexp  39273  climsuse  39276  climrecf  39277  climinff  39279  climaddf  39283  mullimc  39284  idlimc  39294  limcperiod  39296  neglimc  39315  addlimc  39316  0ellimcdiv  39317  fnlimfv  39331  climreclf  39332  fnlimcnv  39335  fnlimfvre  39342  fnlimfvre2  39345  fnlimf  39346  fnlimabslt  39347  climfveqf  39348  climmptf  39349  climeldmeqf  39351  limsupref  39353  limsupbnd1f  39354  climbddf  39355  climeqf  39356  limsuppnfd  39370  climinf2  39375  limsuppnf  39379  limsupubuz  39381  climinfmpt  39383  limsupmnf  39389  limsupequz  39391  limsupre2  39393  limsupmnfuz  39395  limsupre3  39401  limsupre3uz  39404  limsupreuz  39405  cncfshift  39422  icccncfext  39435  cncficcgt0  39436  cncfiooicclem1  39441  dvnmul  39495  dvnprodlem1  39498  itgsubsticclem  39528  stoweidlem3  39557  stoweidlem23  39577  stoweidlem26  39580  stoweidlem28  39582  stoweidlem29  39583  stoweidlem31  39585  stoweidlem34  39588  stoweidlem36  39590  stoweidlem42  39596  stoweidlem48  39602  stoweidlem51  39605  stoweidlem52  39606  stoweidlem59  39613  wallispilem5  39623  stirlinglem4  39631  stirlinglem11  39638  stirlinglem12  39639  stirlinglem13  39640  stirlinglem14  39641  stirlinglem15  39642  fourierdlem20  39681  fourierdlem31  39692  fourierdlem79  39739  fourierdlem89  39749  fourierdlem91  39751  fourierdlem112  39772  fourierdlem115  39775  fourierd  39776  fourierclimd  39777  etransclem2  39790  etransclem48  39836  sge0revalmpt  39932  sge0fsummpt  39944  sge0iunmptlemfi  39967  sge0iunmptlemre  39969  sge0iunmpt  39972  sge0xadd  39989  sge0fsummptf  39990  sge0gtfsumgt  39997  iundjiun  40014  meadjiun  40020  voliunsge0lem  40026  omeiunle  40068  omeiunltfirp  40070  ovncvrrp  40115  vonioo  40233  vonicc  40236  vonn0ioo2  40241  vonn0icc2  40243  pimltmnf2  40248  pimgtpnf2  40254  pimltpnf2  40260  pimgtmnf2  40261  pimdecfgtioc  40262  issmff  40280  smfpimltxrmpt  40304  smfpreimagtf  40313  smflim  40322  smfpimgtxr  40325  smfpimgtxrmpt  40329  smfmullem4  40338  smflim2  40349  smfpimcclem  40350  smfpimcc  40351  smfsup  40357  smfsupmpt  40358  smfsupxr  40359  smfinflem  40360  smfinf  40361  smfinfmpt  40362  smflimsuplem2  40364  smflimsuplem5  40367  smflimsuplem7  40369  smflimsup  40371  nfafv  40550  nfsetrecs  41756  setrec2fun  41762
  Copyright terms: Public domain W3C validator