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

Theorem nfcxfr 2759
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 2758 . 2 (𝑥𝐴𝑥𝐵)
41, 3mpbir 221 1 𝑥𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  wnfc 2748
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-12 2044  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-cleq 2614  df-clel 2617  df-nfc 2750
This theorem is referenced by:  nfrab1  3114  nfrab  3115  nfdif  3714  nfun  3752  nfin  3803  nfsymdif  3831  nfpw  4148  nfpr  4208  nfsn  4218  nfop  4391  nfuni  4413  nfint  4456  nfiun  4519  nfiin  4520  nfiu1  4521  nfii1  4522  nfopab  4685  nfopab1  4686  nfopab2  4687  nfmpt  4711  nfmpt1  4712  nfxp  5107  nfco  5252  nfcnv  5266  nfdm  5332  nfrn  5333  nfres  5363  nfima  5438  nfpred  5649  nfsuc  5760  nfiota1  5817  nffv  6160  fvmptss  6254  fvmptf  6262  fvopab5  6270  ralrnmpt  6329  f1ompt  6343  f1mpt  6478  fliftfun  6522  nfriota1  6578  riotaprop  6595  nfoprab1  6664  nfoprab2  6665  nfoprab3  6666  nfoprab  6667  nfmpt21  6682  nfmpt22  6683  nfmpt2  6684  ovmpt2s  6744  ov2gf  6745  ov3  6757  nftpos  7339  fvmpt2curryd  7349  nfwrecs  7361  nfrecs  7423  nfrdg  7462  rdgsucmptf  7476  rdgsucmptnf  7477  frsucmpt  7485  frsucmptn  7486  nfixp  7878  nfixp1  7879  xpcomco  8001  nfsup  8308  nfinf  8339  nfoi  8370  cnfcom3clem  8553  dfac8clem  8806  iunfo  9312  pwfseqlem2  9432  pwfseqlem4a  9434  pwfseqlem4  9435  reclem2pr  9821  nfseq  12758  nfwrd  13279  nfsum1  14361  nfsum  14362  nfcprod1  14572  nfcprod  14573  ptbasfi  21303  mbfsup  23350  itg1climres  23400  itg2splitlem  23434  itg2split  23435  nfitg1  23459  nfitg  23460  lgamgulm2  24675  lgseisenlem2  25014  lfgrnloop  25928  cnlnadjlem5  28797  nfesum1  29901  nfesum2  29902  ballotlem7  30396  bnj1230  30608  bnj1476  30652  bnj900  30734  bnj958  30745  bnj1000  30746  bnj1014  30765  bnj1123  30789  bnj1307  30826  bnj1321  30830  bnj1384  30835  bnj1398  30837  bnj1408  30839  bnj1444  30846  bnj1445  30847  bnj1446  30848  bnj1447  30849  bnj1448  30850  bnj1449  30851  bnj1466  30856  bnj1467  30857  bnj1518  30867  bnj1519  30868  bnj1520  30869  bnj1525  30872  bnj1523  30874  cvmcov  30980  nfwsuc  31492  nfwlim  31496  nfaltop  31756  topdifinfindis  32853  finxpreclem6  32892  sdclem1  33198  riotasv2s  33751  cdleme26ee  35155  cdlemefs32sn1aw  35209  cdleme43fsv1snlem  35215  cdleme41sn3a  35228  cdleme32d  35239  cdleme32f  35241  cdleme40m  35262  cdleme40n  35263  ltrniotaval  35376  cdlemksv2  35642  cdlemkuv2  35662  cdlemk36  35708  cdlemk38  35710  cdlemkid  35731  cdlemk19x  35738  cdlemk11t  35741  areaquad  37310  binomcxplemdvbinom  38061  binomcxplemdvsum  38063  binomcxplemnotnn0  38064  refsum2cnlem1  38706  eliuniincex  38804  suprnmpt  38852  wessf1ornlem  38868  disjrnmpt2  38872  fompt  38876  allbutfi  39103  allbutfiinf  39134  fmuldfeqlem1  39241  fmuldfeq  39242  mullimc  39275  idlimc  39285  limcperiod  39287  neglimc  39306  addlimc  39307  0ellimcdiv  39308  fnlimcnv  39326  fnlimfvre  39333  fnlimfvre2  39336  fnlimf  39337  fnlimabslt  39338  cncfmptssg  39409  cncfshift  39413  cncficcgt0  39427  cncfiooicclem1  39432  dvnmul  39486  dvnprodlem1  39489  itgsinexplem1  39497  itgsubsticclem  39519  stoweidlem14  39559  stoweidlem16  39561  stoweidlem18  39563  stoweidlem22  39567  stoweidlem26  39571  stoweidlem27  39572  stoweidlem31  39576  stoweidlem32  39577  stoweidlem34  39579  stoweidlem35  39580  stoweidlem40  39585  stoweidlem41  39586  stoweidlem42  39587  stoweidlem44  39589  stoweidlem45  39590  stoweidlem46  39591  stoweidlem47  39592  stoweidlem48  39593  stoweidlem50  39595  stoweidlem51  39596  stoweidlem52  39597  stoweidlem53  39598  stoweidlem54  39599  stoweidlem57  39602  stoweidlem59  39604  stoweidlem62  39607  wallispilem5  39614  stirlinglem4  39622  stirlinglem5  39623  stirlinglem8  39626  stirlinglem11  39629  stirlinglem12  39630  stirlinglem13  39631  stirlinglem14  39632  stirlinglem15  39633  fourierdlem20  39672  fourierdlem31  39683  fourierdlem68  39719  fourierdlem80  39731  fourierdlem89  39740  fourierdlem91  39742  fourierdlem103  39754  fourierdlem104  39755  fourierdlem112  39763  fourierdlem115  39766  fourierd  39767  fourierclimd  39768  etransclem48  39827  iundjiun  40005  ovnlerp  40104  ovncvrrp  40106  ovnhoilem1  40143  opnvonmbllem1  40174  iunhoiioolem  40217  vonioo  40224  vonicc  40227  pimdecfgtioc  40253  pimincfltioc  40254  pimdecfgtioo  40255  pimincfltioo  40256  issmff  40271  incsmflem  40278  smfconst  40286  decsmflem  40302  smfpreimagtf  40304  smflimlem2  40308  smflim  40313  smfpimgtxr  40316  smfresal  40323  smfmullem2  40327  smfmullem4  40329  smfpimbor1lem2  40334  smflim2  40340  smfpimcclem  40341  smflimmpt  40344  smfsup  40348  smfsupmpt  40349  smfsupxr  40350  smfinf  40352  smfinfmpt  40353  smflimsuplem2  40355  smflimsuplem5  40358  smflimsup  40362  nfafv  40541  nfaov  40584  prmdvdsfmtnof1lem1  40816  nfsetrecs  41747
  Copyright terms: Public domain W3C validator