Theorem nfcxfr 2896

Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypotheses

Ref	Expression
nfcxfr.1	⊢ 𝐴 = 𝐵
nfcxfr.2	⊢ Ⅎ𝑥𝐵

Assertion

Ref	Expression
nfcxfr	⊢ Ⅎ𝑥𝐴

Proof of Theorem nfcxfr

Step	Hyp	Ref	Expression
1		nfcxfr.2	. 2 ⊢ Ⅎ𝑥𝐵
2		nfcxfr.1	. . 3 ⊢ 𝐴 = 𝐵
3	2	nfceqi 2895	. 2 ⊢ (Ⅎ𝑥𝐴 ↔ Ⅎ𝑥𝐵)
4	1, 3	mpbir 231	1 ⊢ Ⅎ𝑥𝐴

Syntax hints:   = wceq 1542  Ⅎwnfc 2883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-nf 1786  df-cleq 2728  df-clel 2811  df-nfc 2885

This theorem is referenced by:  nfrab1  3409  nfrabw  3426  nfrab  3427  nfdifOLD  4070  nfunOLD  4111  nfinOLD  4165  nfsymdif  4197  nfpw  4560  nfpr  4636  nfsn  4651  nfop  4832  nfint  4899  nfiun  4965  nfiin  4966  nfiung  4967  nfiing  4968  nfiu1OLD  4970  nfii1  4971  nfopab1  5155  nfopab2  5156  nfmpt  5183  nfmpt1  5184  nfxp  5664  nfco  5820  nfcnv  5833  nfdm  5906  nfrn  5907  nfres  5946  nfima  6033  nfpred  6270  nfsuc  6397  nfiota1  6456  nffv  6850  fvmptss  6960  fvmptf  6969  fvopab5  6981  ralrnmptw  7046  ralrnmpt  7048  f1ompt  7063  fompt  7070  f1mpt  7216  fliftfun  7267  nfriota1  7331  riotaprop  7351  nfoprab1  7428  nfoprab2  7429  nfoprab3  7430  nfoprab  7431  nfmpo1  7447  nfmpo2  7448  nfmpo  7449  ovmpos  7515  ov2gf  7516  ov3  7530  nfof  7637  nfofr  7638  nftpos  8211  fvmpocurryd  8221  nffrecs  8233  nfwrecs  8264  nfrecs  8314  nfrdg  8353  rdgsucmptf  8367  rdgsucmptnf  8368  frsucmpt  8377  frsucmptn  8378  nfixpw  8864  nfixp  8865  nfixp1  8866  xpcomco  9005  nfsup  9364  nfinf  9396  nfoi  9429  cnfcom3clem  9626  ttrclselem1  9646  ttrclselem2  9647  nfdju  9831  dfac8clem  9954  iunfo  10461  pwfseqlem2  10582  pwfseqlem4a  10584  pwfseqlem4  10585  reclem2pr  10971  nfseq  13973  nfwrd  14505  nfsum1  15652  nfsum  15653  nfcprod1  15873  nfcprod  15874  symgval  19346  ptbasfi  23546  mbfsup  25631  itg1climres  25681  itg2splitlem  25715  itg2split  25716  nfitg1  25741  nfitg  25742  lgamgulm2  26999  lgseisenlem2  27339  nosupbnd2  27680  noinfbnd2  27695  nfseqs  28279  lfgrnloop  29194  numclwlk2lem2f1o  30449  cnlnadjlem5  32142  2ndresdju  32722  nfesum1  34184  nfesum2  34185  ballotlem7  34680  bnj1230  34944  bnj1476  34989  bnj900  35071  bnj958  35082  bnj1000  35083  bnj1014  35103  bnj1123  35128  bnj1307  35165  bnj1321  35169  bnj1384  35174  bnj1398  35176  bnj1408  35178  bnj1444  35185  bnj1445  35186  bnj1446  35187  bnj1447  35188  bnj1448  35189  bnj1449  35190  bnj1466  35195  bnj1467  35196  bnj1518  35206  bnj1519  35207  bnj1520  35208  bnj1525  35211  bnj1523  35213  cvmcov  35445  nfwsuc  35998  nfwlim  36002  nfaltop  36162  nfttc  36673  currysetlem1  37254  topdifinfindis  37662  rdgssun  37694  exrecfnlem  37695  finxpreclem6  37712  sdclem1  38064  riotasv2s  39404  cdleme26ee  40806  cdlemefs32sn1aw  40860  cdleme43fsv1snlem  40866  cdleme41sn3a  40879  cdleme32d  40890  cdleme32f  40892  cdleme40m  40913  cdleme40n  40914  ltrniotaval  41027  cdlemksv2  41293  cdlemkuv2  41313  cdlemk36  41359  cdlemk38  41361  cdlemkid  41382  cdlemk19x  41389  cdlemk11t  41392  areaquad  43644  nfscott  44666  nfcoll  44683  binomcxplemdvbinom  44780  binomcxplemdvsum  44782  binomcxplemnotnn0  44783  refsum2cnlem1  45468  eliuniincex  45539  disjrnmpt2  45618  rnmptssbi  45689  allbutfi  45822  allbutfiinf  45848  rexanuz2nf  45920  fmuldfeqlem1  46012  fmuldfeq  46013  mullimc  46046  idlimc  46056  limcperiod  46058  neglimc  46075  addlimc  46076  0ellimcdiv  46077  fnlimcnv  46095  fnlimfvre  46102  fnlimfvre2  46105  fnlimf  46106  fnlimabslt  46107  xlimmnfmpt  46271  xlimpnfmpt  46272  cncfmptssg  46299  cncfshift  46302  cncficcgt0  46316  cncfiooicclem1  46321  dvnmul  46371  dvnprodlem1  46374  itgsinexplem1  46382  itgsubsticclem  46403  stoweidlem14  46442  stoweidlem16  46444  stoweidlem18  46446  stoweidlem22  46450  stoweidlem26  46454  stoweidlem27  46455  stoweidlem31  46459  stoweidlem32  46460  stoweidlem34  46462  stoweidlem35  46463  stoweidlem40  46468  stoweidlem41  46469  stoweidlem42  46470  stoweidlem44  46472  stoweidlem45  46473  stoweidlem46  46474  stoweidlem47  46475  stoweidlem48  46476  stoweidlem50  46478  stoweidlem51  46479  stoweidlem52  46480  stoweidlem53  46481  stoweidlem54  46482  stoweidlem57  46485  stoweidlem59  46487  stoweidlem62  46490  wallispilem5  46497  stirlinglem4  46505  stirlinglem5  46506  stirlinglem8  46509  stirlinglem11  46512  stirlinglem12  46513  stirlinglem13  46514  stirlinglem14  46515  stirlinglem15  46516  fourierdlem20  46555  fourierdlem31  46566  fourierdlem68  46602  fourierdlem80  46614  fourierdlem89  46623  fourierdlem91  46625  fourierdlem103  46637  fourierdlem104  46638  fourierdlem112  46646  fourierdlem115  46649  fourierd  46650  fourierclimd  46651  etransclem48  46710  iundjiun  46888  meaiuninc3v  46912  ovnlerp  46990  ovncvrrp  46992  ovnhoilem1  47029  opnvonmbllem1  47060  iunhoiioolem  47103  vonioo  47110  vonicc  47113  pimdecfgtioc  47143  pimincfltioc  47144  pimdecfgtioo  47145  pimincfltioo  47146  issmff  47162  incsmflem  47169  smfpimltxr  47175  smfconst  47177  decsmflem  47194  smfpreimagtf  47196  smflimlem2  47200  smflim  47205  smfpimgtxr  47208  smfresal  47216  smfmullem2  47220  smfmullem4  47222  smfpimbor1lem2  47227  smflim2  47234  smfpimcclem  47235  smflimmpt  47238  smfsup  47242  smfsupmpt  47243  smfsupxr  47244  smfinf  47246  smfinfmpt  47247  smflimsuplem2  47249  smflimsuplem5  47252  smflimsup  47256  smfliminf  47259  smfpimne2  47268  smfdivdmmbl2  47269  fsupdm  47270  fsupdm2  47271  finfdm  47274  finfdm2  47275  nfafv  47584  nfaov  47627  nfafv2  47666  prmdvdsfmtnof1lem1  48047  nfsetrecs  50161