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

Theorem nfcxfr 2911
Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypotheses
Ref Expression
nfceqi.1 𝐴 = 𝐵
nfcxfr.2 𝑥𝐵
Assertion
Ref Expression
nfcxfr 𝑥𝐴

Proof of Theorem nfcxfr
StepHypRef Expression
1 nfcxfr.2 . 2 𝑥𝐵
2 nfceqi.1 . . 3 𝐴 = 𝐵
32nfceqi 2910 . 2 (𝑥𝐴𝑥𝐵)
41, 3mpbir 221 1 𝑥𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1631  wnfc 2900
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-12 2203  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-tru 1634  df-ex 1853  df-nf 1858  df-cleq 2764  df-clel 2767  df-nfc 2902
This theorem is referenced by:  nfrab1  3271  nfrab  3272  nfdif  3882  nfun  3920  nfin  3969  nfsymdif  3997  nfpw  4311  nfpr  4369  nfsn  4379  nfop  4555  nfuni  4580  nfint  4621  nfiun  4682  nfiin  4683  nfiu1  4684  nfii1  4685  nfopab  4852  nfopab1  4853  nfopab2  4854  nfmpt  4880  nfmpt1  4881  nfxp  5282  nfco  5426  nfcnv  5439  nfdm  5505  nfrn  5506  nfres  5536  nfima  5615  nfpred  5828  nfsuc  5939  nfiota1  5996  nffv  6339  fvmptss  6434  fvmptf  6443  fvopab5  6452  ralrnmpt  6511  f1ompt  6524  f1mpt  6661  fliftfun  6705  nfriota1  6761  riotaprop  6778  nfoprab1  6851  nfoprab2  6852  nfoprab3  6853  nfoprab  6854  nfmpt21  6869  nfmpt22  6870  nfmpt2  6871  ovmpt2s  6931  ov2gf  6932  ov3  6944  nfof  7049  nfofr  7050  nftpos  7539  fvmpt2curryd  7549  nfwrecs  7561  nfrecs  7624  nfrdg  7663  rdgsucmptf  7677  rdgsucmptnf  7678  frsucmpt  7686  frsucmptn  7687  nfixp  8081  nfixp1  8082  xpcomco  8206  nfsup  8513  nfinf  8544  nfoi  8575  cnfcom3clem  8766  nfdju  8934  dfac8clem  9055  iunfo  9563  pwfseqlem2  9683  pwfseqlem4a  9685  pwfseqlem4  9686  reclem2pr  10072  nfseq  13018  nfwrd  13529  nfsum1  14628  nfsum  14629  nfcprod1  14847  nfcprod  14848  ptbasfi  21605  mbfsup  23651  itg1climres  23701  itg2splitlem  23735  itg2split  23736  nfitg1  23760  nfitg  23761  lgamgulm2  24983  lgseisenlem2  25322  lfgrnloop  26241  numclwwlk1lem2OLD  27547  numclwlk2lem2f1o  27570  numclwlk2lem2f1oOLD  27577  cnlnadjlem5  29270  nfesum1  30442  nfesum2  30443  ballotlem7  30937  bnj1230  31211  bnj1476  31255  bnj900  31337  bnj958  31348  bnj1000  31349  bnj1014  31368  bnj1123  31392  bnj1307  31429  bnj1321  31433  bnj1384  31438  bnj1398  31440  bnj1408  31442  bnj1444  31449  bnj1445  31450  bnj1446  31451  bnj1447  31452  bnj1448  31453  bnj1449  31454  bnj1466  31459  bnj1467  31460  bnj1518  31470  bnj1519  31471  bnj1520  31472  bnj1525  31475  bnj1523  31477  cvmcov  31583  nfwsuc  32100  nfwlim  32104  nffrecs  32115  nosupbnd2  32199  nfaltop  32424  topdifinfindis  33531  finxpreclem6  33570  cnfinltrel  33578  sdclem1  33871  riotasv2s  34766  cdleme26ee  36169  cdlemefs32sn1aw  36223  cdleme43fsv1snlem  36229  cdleme41sn3a  36242  cdleme32d  36253  cdleme32f  36255  cdleme40m  36276  cdleme40n  36277  ltrniotaval  36390  cdlemksv2  36656  cdlemkuv2  36676  cdlemk36  36722  cdlemk38  36724  cdlemkid  36745  cdlemk19x  36752  cdlemk11t  36755  areaquad  38328  binomcxplemdvbinom  39078  binomcxplemdvsum  39080  binomcxplemnotnn0  39081  refsum2cnlem1  39718  eliuniincex  39813  suprnmpt  39875  wessf1ornlem  39891  disjrnmpt2  39895  fompt  39899  rnmptssbi  39995  allbutfi  40132  allbutfiinf  40163  fmuldfeqlem1  40332  fmuldfeq  40333  mullimc  40366  idlimc  40376  limcperiod  40378  neglimc  40397  addlimc  40398  0ellimcdiv  40399  fnlimcnv  40417  fnlimfvre  40424  fnlimfvre2  40427  fnlimf  40428  fnlimabslt  40429  xlimmnfmpt  40587  xlimpnfmpt  40588  cncfmptssg  40601  cncfshift  40605  cncficcgt0  40619  cncfiooicclem1  40624  dvnmul  40676  dvnprodlem1  40679  itgsinexplem1  40687  itgsubsticclem  40708  stoweidlem14  40748  stoweidlem16  40750  stoweidlem18  40752  stoweidlem22  40756  stoweidlem26  40760  stoweidlem27  40761  stoweidlem31  40765  stoweidlem32  40766  stoweidlem34  40768  stoweidlem35  40769  stoweidlem40  40774  stoweidlem41  40775  stoweidlem42  40776  stoweidlem44  40778  stoweidlem45  40779  stoweidlem46  40780  stoweidlem47  40781  stoweidlem48  40782  stoweidlem50  40784  stoweidlem51  40785  stoweidlem52  40786  stoweidlem53  40787  stoweidlem54  40788  stoweidlem57  40791  stoweidlem59  40793  stoweidlem62  40796  wallispilem5  40803  stirlinglem4  40811  stirlinglem5  40812  stirlinglem8  40815  stirlinglem11  40818  stirlinglem12  40819  stirlinglem13  40820  stirlinglem14  40821  stirlinglem15  40822  fourierdlem20  40861  fourierdlem31  40872  fourierdlem68  40908  fourierdlem80  40920  fourierdlem89  40929  fourierdlem91  40931  fourierdlem103  40943  fourierdlem104  40944  fourierdlem112  40952  fourierdlem115  40955  fourierd  40956  fourierclimd  40957  etransclem48  41016  iundjiun  41194  meaiuninc3v  41218  ovnlerp  41296  ovncvrrp  41298  ovnhoilem1  41335  opnvonmbllem1  41366  iunhoiioolem  41409  vonioo  41416  vonicc  41419  pimdecfgtioc  41445  pimincfltioc  41446  pimdecfgtioo  41447  pimincfltioo  41448  issmff  41463  incsmflem  41470  smfconst  41478  decsmflem  41494  smfpreimagtf  41496  smflimlem2  41500  smflim  41505  smfpimgtxr  41508  smfresal  41515  smfmullem2  41519  smfmullem4  41521  smfpimbor1lem2  41526  smflim2  41532  smfpimcclem  41533  smflimmpt  41536  smfsup  41540  smfsupmpt  41541  smfsupxr  41542  smfinf  41544  smfinfmpt  41545  smflimsuplem2  41547  smflimsuplem5  41550  smflimsup  41554  smfliminf  41557  nfafv  41736  nfaov  41779  prmdvdsfmtnof1lem1  42024  nfsetrecs  42961
  Copyright terms: Public domain W3C validator