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

Theorem nfcxfr 2944
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 2943 . 2 (𝑥𝐴𝑥𝐵)
41, 3mpbir 222 1 𝑥𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1637  wnfc 2933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-12 2214  ax-ext 2782
This theorem depends on definitions:  df-bi 198  df-an 385  df-tru 1641  df-ex 1860  df-nf 1864  df-cleq 2797  df-clel 2800  df-nfc 2935
This theorem is referenced by:  nfrab1  3309  nfrab  3310  nfdif  3928  nfun  3966  nfin  4015  nfsymdif  4044  nfpw  4363  nfpr  4422  nfsn  4432  nfop  4609  nfuni  4634  nfint  4677  nfiun  4738  nfiin  4739  nfiu1  4740  nfii1  4741  nfopab  4910  nfopab1  4911  nfopab2  4912  nfmpt  4938  nfmpt1  4939  nfxp  5341  nfco  5487  nfcnv  5500  nfdm  5566  nfrn  5567  nfres  5597  nfima  5682  nfpred  5896  nfsuc  6007  nfiota1  6064  nffv  6416  fvmptss  6511  fvmptf  6520  fvopab5  6529  ralrnmpt  6588  f1ompt  6601  f1mpt  6740  fliftfun  6784  nfriota1  6840  riotaprop  6857  nfoprab1  6932  nfoprab2  6933  nfoprab3  6934  nfoprab  6935  nfmpt21  6950  nfmpt22  6951  nfmpt2  6952  ovmpt2s  7012  ov2gf  7013  ov3  7025  nfof  7130  nfofr  7131  nftpos  7620  fvmpt2curryd  7630  nfwrecs  7642  nfrecs  7705  nfrdg  7744  rdgsucmptf  7758  rdgsucmptnf  7759  frsucmpt  7767  frsucmptn  7768  nfixp  8162  nfixp1  8163  xpcomco  8287  nfsup  8594  nfinf  8625  nfoi  8656  cnfcom3clem  8847  nfdju  9015  dfac8clem  9136  iunfo  9644  pwfseqlem2  9764  pwfseqlem4a  9766  pwfseqlem4  9767  reclem2pr  10153  nfseq  13032  nfwrd  13542  nfsum1  14641  nfsum  14642  nfcprod1  14859  nfcprod  14860  ptbasfi  21596  mbfsup  23643  itg1climres  23693  itg2splitlem  23727  itg2split  23728  nfitg1  23752  nfitg  23753  lgamgulm2  24974  lgseisenlem2  25313  lfgrnloop  26232  numclwwlk1lem2OLD  27538  numclwlk2lem2f1o  27557  numclwlk2lem2f1oOLD  27564  cnlnadjlem5  29256  nfesum1  30425  nfesum2  30426  ballotlem7  30920  bnj1230  31194  bnj1476  31238  bnj900  31320  bnj958  31331  bnj1000  31332  bnj1014  31351  bnj1123  31375  bnj1307  31412  bnj1321  31416  bnj1384  31421  bnj1398  31423  bnj1408  31425  bnj1444  31432  bnj1445  31433  bnj1446  31434  bnj1447  31435  bnj1448  31436  bnj1449  31437  bnj1466  31442  bnj1467  31443  bnj1518  31453  bnj1519  31454  bnj1520  31455  bnj1525  31458  bnj1523  31460  cvmcov  31566  nfwsuc  32082  nfwlim  32086  nffrecs  32097  nosupbnd2  32181  nfaltop  32406  topdifinfindis  33508  finxpreclem6  33547  cnfinltrel  33555  sdclem1  33848  riotasv2s  34735  cdleme26ee  36139  cdlemefs32sn1aw  36193  cdleme43fsv1snlem  36199  cdleme41sn3a  36212  cdleme32d  36223  cdleme32f  36225  cdleme40m  36246  cdleme40n  36247  ltrniotaval  36360  cdlemksv2  36626  cdlemkuv2  36646  cdlemk36  36692  cdlemk38  36694  cdlemkid  36715  cdlemk19x  36722  cdlemk11t  36725  areaquad  38300  binomcxplemdvbinom  39050  binomcxplemdvsum  39052  binomcxplemnotnn0  39053  refsum2cnlem1  39688  eliuniincex  39782  suprnmpt  39842  wessf1ornlem  39858  disjrnmpt2  39862  fompt  39866  rnmptssbi  39958  allbutfi  40093  allbutfiinf  40124  fmuldfeqlem1  40292  fmuldfeq  40293  mullimc  40326  idlimc  40336  limcperiod  40338  neglimc  40357  addlimc  40358  0ellimcdiv  40359  fnlimcnv  40377  fnlimfvre  40384  fnlimfvre2  40387  fnlimf  40388  fnlimabslt  40389  xlimmnfmpt  40547  xlimpnfmpt  40548  cncfmptssg  40561  cncfshift  40565  cncficcgt0  40579  cncfiooicclem1  40584  dvnmul  40636  dvnprodlem1  40639  itgsinexplem1  40647  itgsubsticclem  40668  stoweidlem14  40708  stoweidlem16  40710  stoweidlem18  40712  stoweidlem22  40716  stoweidlem26  40720  stoweidlem27  40721  stoweidlem31  40725  stoweidlem32  40726  stoweidlem34  40728  stoweidlem35  40729  stoweidlem40  40734  stoweidlem41  40735  stoweidlem42  40736  stoweidlem44  40738  stoweidlem45  40739  stoweidlem46  40740  stoweidlem47  40741  stoweidlem48  40742  stoweidlem50  40744  stoweidlem51  40745  stoweidlem52  40746  stoweidlem53  40747  stoweidlem54  40748  stoweidlem57  40751  stoweidlem59  40753  stoweidlem62  40756  wallispilem5  40763  stirlinglem4  40771  stirlinglem5  40772  stirlinglem8  40775  stirlinglem11  40778  stirlinglem12  40779  stirlinglem13  40780  stirlinglem14  40781  stirlinglem15  40782  fourierdlem20  40821  fourierdlem31  40832  fourierdlem68  40868  fourierdlem80  40880  fourierdlem89  40889  fourierdlem91  40891  fourierdlem103  40903  fourierdlem104  40904  fourierdlem112  40912  fourierdlem115  40915  fourierd  40916  fourierclimd  40917  etransclem48  40976  iundjiun  41154  meaiuninc3v  41178  ovnlerp  41256  ovncvrrp  41258  ovnhoilem1  41295  opnvonmbllem1  41326  iunhoiioolem  41369  vonioo  41376  vonicc  41379  pimdecfgtioc  41405  pimincfltioc  41406  pimdecfgtioo  41407  pimincfltioo  41408  issmff  41423  incsmflem  41430  smfconst  41438  decsmflem  41454  smfpreimagtf  41456  smflimlem2  41460  smflim  41465  smfpimgtxr  41468  smfresal  41475  smfmullem2  41479  smfmullem4  41481  smfpimbor1lem2  41486  smflim2  41492  smfpimcclem  41493  smflimmpt  41496  smfsup  41500  smfsupmpt  41501  smfsupxr  41502  smfinf  41504  smfinfmpt  41505  smflimsuplem2  41507  smflimsuplem5  41510  smflimsup  41514  smfliminf  41517  nfafv  41723  nfaov  41766  nfafv2  41805  prmdvdsfmtnof1lem1  42069  nfsetrecs  42999
  Copyright terms: Public domain W3C validator