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

Theorem nffv 6160
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 5860 . 2 (𝐹𝐴) = (℩𝑦𝐴𝐹𝑦)
2 nffv.2 . . . 4 𝑥𝐴
3 nffv.1 . . . 4 𝑥𝐹
4 nfcv 2761 . . . 4 𝑥𝑦
52, 3, 4nfbr 4664 . . 3 𝑥 𝐴𝐹𝑦
65nfiota 5819 . 2 𝑥(℩𝑦𝐴𝐹𝑦)
71, 6nfcxfr 2759 1 𝑥(𝐹𝐴)
Colors of variables: wff setvar class
Syntax hints:  wnfc 2748   class class class wbr 4618  cio 5813  cfv 5852
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 2912  df-rex 2913  df-rab 2916  df-v 3191  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-iota 5815  df-fv 5860
This theorem is referenced by:  nffvmpt1  6161  nffvd  6162  dffn5f  6214  fvmptss  6254  fvmptex  6256  fvmptf  6262  fvmptnf  6263  eqfnfv2f  6276  ralrnmpt  6329  ffnfvf  6350  funiunfvf  6467  dff13f  6473  nfiso  6532  nfwrecs  7361  nfrdg  7462  rdgsucmptf  7476  rdgsucmptnf  7477  frsucmpt  7485  frsucmptn  7486  rankidb  8615  rankval4  8682  dfac8clem  8807  cardaleph  8864  hsmexlem2  9201  axcc2  9211  uniimadomf  9319  nfseq  12759  seqof2  12807  rlim2  14169  nfsum1  14362  nfsum  14363  sumeq2ii  14365  fsumrelem  14477  o1fsum  14483  nfcprod1  14576  nfcprod  14577  fprodefsum  14761  prdsbas3  16073  prdsdsval2  16076  yonedalem4b  16848  gsum2d2lem  18304  coe1fzgsumdlem  19603  evl1gsumdlem  19652  ptcldmpt  21340  ptcnp  21348  cnmpt11  21389  cnmpt21  21397  cnmptk2  21412  prdsdsf  22095  prdsxmet  22097  ovolfiniun  23192  ovoliunlem3  23195  ovoliun  23196  ovoliun2  23197  ovoliunnul  23198  volfiniun  23238  voliun  23245  mbfsup  23354  mbflim  23358  itg2splitlem  23438  itg2split  23439  itg2cnlem1  23451  isibl2  23456  nfitg1  23463  nfitg  23464  cbvitg  23465  itgabs  23524  dvlipcn  23678  lhop2  23699  dvfsumabs  23707  dvfsumrlim  23715  itgparts  23731  itgsubstlem  23732  ulmss  24072  itgulm2  24084  lgamgulmlem2  24673  lgamgulmlem6  24677  lgamgulm2  24679  lgseisenlem2  25018  dchrisumlem3  25097  cnlnadjlem5  28800  dfimafnf  29302  esumfzf  29936  voliune  30097  volfiniune  30098  bnj1534  30666  bnj1542  30670  bnj958  30753  bnj1000  30754  bnj1446  30856  bnj1447  30857  bnj1448  30858  bnj1466  30864  bnj1467  30865  bnj1519  30876  bnj1520  30877  bnj1529  30881  cvmcov  30988  trpredlem1  31463  trpredrec  31474  sltval2  31545  nobndlem5  31594  finxpreclem2  32894  finxpreclem6  32900  poimirlem23  33099  poimirlem27  33103  itgabsnc  33146  riotaocN  34011  cdleme32d  35247  cdleme32f  35249  ltrniotaval  35384  cdlemksv2  35650  cdlemkuv2  35670  cdlemk36  35716  cdlemk38  35718  cdlemk19x  35746  cdlemk11t  35749  mzpsubst  36826  aomclem8  37146  binomcxplemdvbinom  38069  binomcxplemdvsum  38071  binomcxplemnotnn0  38072  evth2f  38692  fvelrnbf  38695  evthf  38704  rfcnpre3  38710  rfcnpre4  38711  rfcnnnub  38713  refsum2cnlem1  38714  dffo3f  38869  fvelimad  38964  allbutfiinf  39142  fmul01  39244  fmuldfeqlem1  39246  fmuldfeq  39247  fmul01lt1lem1  39248  fmul01lt1lem2  39249  fmul01lt1  39250  cncfmptss  39251  mulc1cncfg  39253  expcnfg  39255  fprodabs2  39259  climmulf  39268  climexp  39269  climsuse  39272  climrecf  39273  climinff  39275  climaddf  39279  mullimc  39280  idlimc  39290  limcperiod  39292  neglimc  39311  addlimc  39312  0ellimcdiv  39313  fnlimfv  39327  climreclf  39328  fnlimcnv  39331  fnlimfvre  39338  fnlimfvre2  39341  fnlimf  39342  fnlimabslt  39343  climfveqf  39344  climmptf  39345  climeldmeqf  39347  limsupref  39349  limsupbnd1f  39350  climbddf  39351  climeqf  39352  limsuppnfd  39366  climinf2  39371  limsuppnf  39375  limsupubuz  39377  climinfmpt  39379  limsupmnf  39385  limsupequz  39387  limsupre2  39389  limsupmnfuz  39391  limsupre3  39397  limsupre3uz  39400  limsupreuz  39401  cncfshift  39418  icccncfext  39431  cncficcgt0  39432  cncfiooicclem1  39437  dvnmul  39491  dvnprodlem1  39494  itgsubsticclem  39524  stoweidlem3  39553  stoweidlem23  39573  stoweidlem26  39576  stoweidlem28  39578  stoweidlem29  39579  stoweidlem31  39581  stoweidlem34  39584  stoweidlem36  39586  stoweidlem42  39592  stoweidlem48  39598  stoweidlem51  39601  stoweidlem52  39602  stoweidlem59  39609  wallispilem5  39619  stirlinglem4  39627  stirlinglem11  39634  stirlinglem12  39635  stirlinglem13  39636  stirlinglem14  39637  stirlinglem15  39638  fourierdlem20  39677  fourierdlem31  39688  fourierdlem79  39735  fourierdlem89  39745  fourierdlem91  39747  fourierdlem112  39768  fourierdlem115  39771  fourierd  39772  fourierclimd  39773  etransclem2  39786  etransclem48  39832  sge0revalmpt  39928  sge0fsummpt  39940  sge0iunmptlemfi  39963  sge0iunmptlemre  39965  sge0iunmpt  39968  sge0xadd  39985  sge0fsummptf  39986  sge0gtfsumgt  39993  iundjiun  40010  meadjiun  40016  voliunsge0lem  40022  omeiunle  40064  omeiunltfirp  40066  ovncvrrp  40111  vonioo  40229  vonicc  40232  vonn0ioo2  40237  vonn0icc2  40239  pimltmnf2  40244  pimgtpnf2  40250  pimltpnf2  40256  pimgtmnf2  40257  pimdecfgtioc  40258  issmff  40276  smfpimltxrmpt  40300  smfpreimagtf  40309  smflim  40318  smfpimgtxr  40321  smfpimgtxrmpt  40325  smfmullem4  40334  smflim2  40345  smfpimcclem  40346  smfpimcc  40347  smfsup  40353  smfsupmpt  40354  smfsupxr  40355  smfinflem  40356  smfinf  40357  smfinfmpt  40358  smflimsuplem2  40360  smflimsuplem5  40363  smflimsuplem7  40365  smflimsup  40367  nfafv  40546  nfsetrecs  41752  setrec2fun  41758
  Copyright terms: Public domain W3C validator