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

Theorem nffv 6351
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 6049 . 2 (𝐹𝐴) = (℩𝑦𝐴𝐹𝑦)
2 nffv.2 . . . 4 𝑥𝐴
3 nffv.1 . . . 4 𝑥𝐹
4 nfcv 2894 . . . 4 𝑥𝑦
52, 3, 4nfbr 4843 . . 3 𝑥 𝐴𝐹𝑦
65nfiota 6008 . 2 𝑥(℩𝑦𝐴𝐹𝑦)
71, 6nfcxfr 2892 1 𝑥(𝐹𝐴)
Colors of variables: wff setvar class
Syntax hints:  wnfc 2881   class class class wbr 4796  cio 6002  cfv 6041
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ral 3047  df-rex 3048  df-rab 3051  df-v 3334  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-if 4223  df-sn 4314  df-pr 4316  df-op 4320  df-uni 4581  df-br 4797  df-iota 6004  df-fv 6049
This theorem is referenced by:  nffvmpt1  6352  nffvd  6353  dffn5f  6406  fvmptss  6446  fvmptex  6448  fvmptf  6455  fvmptnf  6456  eqfnfv2f  6470  ralrnmpt  6523  ffnfvf  6544  funiunfvf  6662  dff13f  6668  nfiso  6727  nfwrecs  7570  nfrdg  7671  rdgsucmptf  7685  rdgsucmptnf  7686  frsucmpt  7694  frsucmptn  7695  rankidb  8828  rankval4  8895  dfac8clem  9037  cardaleph  9094  hsmexlem2  9433  axcc2  9443  uniimadomf  9551  nfseq  12997  seqof2  13045  rlim2  14418  nfsum1  14611  nfsum  14612  sumeq2ii  14614  fsumrelem  14730  o1fsum  14736  nfcprod1  14831  nfcprod  14832  fprodefsum  15016  prdsbas3  16335  prdsdsval2  16338  yonedalem4b  17109  gsum2d2lem  18564  coe1fzgsumdlem  19865  evl1gsumdlem  19914  ptcldmpt  21611  ptcnp  21619  cnmpt11  21660  cnmpt21  21668  cnmptk2  21683  prdsdsf  22365  prdsxmet  22367  ovolfiniun  23461  ovoliunlem3  23464  ovoliun  23465  ovoliun2  23466  ovoliunnul  23467  volfiniun  23507  voliun  23514  mbfsup  23622  mbflim  23626  itg2splitlem  23706  itg2split  23707  itg2cnlem1  23719  isibl2  23724  nfitg1  23731  nfitg  23732  cbvitg  23733  itgabs  23792  dvlipcn  23948  lhop2  23969  dvfsumabs  23977  dvfsumrlim  23985  itgparts  24001  itgsubstlem  24002  ulmss  24342  itgulm2  24354  lgamgulmlem2  24947  lgamgulmlem6  24951  lgamgulm2  24953  lgseisenlem2  25292  dchrisumlem3  25371  cnlnadjlem5  29231  dfimafnf  29737  esumfzf  30432  voliune  30593  volfiniune  30594  bnj1534  31222  bnj1542  31226  bnj958  31309  bnj1000  31310  bnj1446  31412  bnj1447  31413  bnj1448  31414  bnj1466  31420  bnj1467  31421  bnj1519  31432  bnj1520  31433  bnj1529  31437  cvmcov  31544  trpredlem1  32024  trpredrec  32035  sltval2  32107  finxpreclem2  33530  finxpreclem6  33536  poimirlem23  33737  poimirlem27  33741  itgabsnc  33784  riotaocN  34991  cdleme32d  36226  cdleme32f  36228  ltrniotaval  36363  cdlemksv2  36629  cdlemkuv2  36649  cdlemk36  36695  cdlemk38  36697  cdlemk19x  36725  cdlemk11t  36728  mzpsubst  37805  aomclem8  38125  binomcxplemdvbinom  39046  binomcxplemdvsum  39048  binomcxplemnotnn0  39049  evth2f  39665  fvelrnbf  39668  evthf  39677  rfcnpre3  39683  rfcnpre4  39684  rfcnnnub  39686  refsum2cnlem1  39687  dffo3f  39855  fvelimad  39949  allbutfiinf  40137  monoordxr  40203  monoord2xr  40205  fmul01  40307  fmuldfeqlem1  40309  fmuldfeq  40310  fmul01lt1lem1  40311  fmul01lt1lem2  40312  fmul01lt1  40313  cncfmptss  40314  mulc1cncfg  40316  expcnfg  40318  fprodabs2  40322  climmulf  40331  climexp  40332  climsuse  40335  climrecf  40336  climinff  40338  climaddf  40342  mullimc  40343  idlimc  40353  limcperiod  40355  neglimc  40374  addlimc  40375  0ellimcdiv  40376  fnlimfv  40390  climreclf  40391  fnlimcnv  40394  fnlimfvre  40401  fnlimfvre2  40404  fnlimf  40405  fnlimabslt  40406  climfveqf  40407  climmptf  40408  climeldmeqf  40410  limsupref  40412  limsupbnd1f  40413  climbddf  40414  climeqf  40415  limsuppnfd  40429  climinf2  40434  limsuppnf  40438  limsupubuz  40440  climinfmpt  40442  limsupmnf  40448  limsupequz  40450  limsupre2  40452  limsupmnfuz  40454  limsupre3  40460  limsupre3uz  40463  limsupreuz  40464  climuz  40471  lmbr3  40474  limsupgt  40505  liminfvalxr  40510  liminfreuz  40530  liminflt  40532  xlimmnf  40562  xlimpnf  40563  dfxlim2  40569  cncfshift  40582  icccncfext  40595  cncficcgt0  40596  cncfiooicclem1  40601  dvnmul  40653  dvnprodlem1  40656  itgsubsticclem  40686  stoweidlem3  40715  stoweidlem23  40735  stoweidlem26  40738  stoweidlem28  40740  stoweidlem29  40741  stoweidlem31  40743  stoweidlem34  40746  stoweidlem36  40748  stoweidlem42  40754  stoweidlem48  40760  stoweidlem51  40763  stoweidlem52  40764  stoweidlem59  40771  wallispilem5  40781  stirlinglem4  40789  stirlinglem11  40796  stirlinglem12  40797  stirlinglem13  40798  stirlinglem14  40799  stirlinglem15  40800  fourierdlem20  40839  fourierdlem31  40850  fourierdlem79  40897  fourierdlem89  40907  fourierdlem91  40909  fourierdlem112  40930  fourierdlem115  40933  fourierd  40934  fourierclimd  40935  etransclem2  40948  etransclem48  40994  sge0revalmpt  41090  sge0fsummpt  41102  sge0iunmptlemfi  41125  sge0iunmptlemre  41127  sge0iunmpt  41130  sge0xadd  41147  sge0fsummptf  41148  sge0gtfsumgt  41155  iundjiun  41172  meadjiun  41178  voliunsge0lem  41184  meaiunincf  41195  meaiuninc3  41197  omeiunle  41229  omeiunltfirp  41231  ovncvrrp  41276  vonioo  41394  vonicc  41397  vonn0ioo2  41402  vonn0icc2  41404  pimltmnf2  41409  pimgtpnf2  41415  pimltpnf2  41421  pimgtmnf2  41422  pimdecfgtioc  41423  issmff  41441  smfpimltxrmpt  41465  smfpreimagtf  41474  smflim  41483  smfpimgtxr  41486  smfpimgtxrmpt  41490  smfmullem4  41499  smflim2  41510  smfpimcclem  41511  smfpimcc  41512  smfsup  41518  smfsupmpt  41519  smfsupxr  41520  smfinflem  41521  smfinf  41522  smfinfmpt  41523  smflimsuplem2  41525  smflimsuplem5  41528  smflimsuplem7  41530  smflimsup  41532  smfliminf  41535  nfafv  41714  nfsetrecs  42935  setrec2fun  42941
  Copyright terms: Public domain W3C validator