Theorem nfcxfr 2900

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 2899	. 2 ⊢ (Ⅎ𝑥𝐴 ↔ Ⅎ𝑥𝐵)
4	1, 3	mpbir 230	1 ⊢ Ⅎ𝑥𝐴

Syntax hints:   = wceq 1541  Ⅎwnfc 2882

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-nf 1786  df-cleq 2723  df-clel 2809  df-nfc 2884

This theorem is referenced by:  nfrab1  3424  nfrabw  3441  nfrabwOLD  3442  nfrab  3444  nfdif  4090  nfun  4130  nfin  4181  nfsymdif  4211  nfpw  4584  nfpr  4656  nfsn  4673  nfop  4851  nfint  4922  nfiun  4989  nfiin  4990  nfiung  4991  nfiing  4992  nfiu1  4993  nfii1  4994  nfopab1  5180  nfopab2  5181  nfmpt  5217  nfmpt1  5218  nfxp  5671  nfco  5826  nfcnv  5839  nfdm  5911  nfrn  5912  nfres  5944  nfima  6026  nfpred  6263  nfsuc  6394  nfiota1  6455  nffv  6857  fvmptss  6965  fvmptf  6974  fvopab5  6985  ralrnmptw  7049  ralrnmpt  7051  f1ompt  7064  f1mpt  7213  fliftfun  7262  nfriota1  7325  riotaprop  7346  nfoprab1  7423  nfoprab2  7424  nfoprab3  7425  nfoprab  7426  nfmpo1  7442  nfmpo2  7443  nfmpo  7444  ovmpos  7508  ov2gf  7509  ov3  7522  nfof  7628  nfofr  7629  nftpos  8197  fvmpocurryd  8207  nffrecs  8219  nfwrecs  8252  nfwrecsOLD  8253  nfrecs  8326  nfrdg  8365  rdgsucmptf  8379  rdgsucmptnf  8380  frsucmpt  8389  frsucmptn  8390  nfixpw  8861  nfixp  8862  nfixp1  8863  xpcomco  9013  nfsup  9396  nfinf  9427  nfoi  9459  cnfcom3clem  9650  ttrclselem1  9670  ttrclselem2  9671  nfdju  9852  dfac8clem  9977  iunfo  10484  pwfseqlem2  10604  pwfseqlem4a  10606  pwfseqlem4  10607  reclem2pr  10993  nfseq  13926  nfwrd  14443  nfsum1  15586  nfsum  15587  nfcprod1  15804  nfcprod  15805  symgval  19164  ptbasfi  22969  mbfsup  25065  itg1climres  25116  itg2splitlem  25150  itg2split  25151  nfitg1  25175  nfitg  25176  lgamgulm2  26422  lgseisenlem2  26761  nosupbnd2  27101  noinfbnd2  27116  lfgrnloop  28139  numclwlk2lem2f1o  29386  cnlnadjlem5  31076  2ndresdju  31632  nfesum1  32728  nfesum2  32729  ballotlem7  33224  bnj1230  33503  bnj1476  33548  bnj900  33630  bnj958  33641  bnj1000  33642  bnj1014  33662  bnj1123  33687  bnj1307  33724  bnj1321  33728  bnj1384  33733  bnj1398  33735  bnj1408  33737  bnj1444  33744  bnj1445  33745  bnj1446  33746  bnj1447  33747  bnj1448  33748  bnj1449  33749  bnj1466  33754  bnj1467  33755  bnj1518  33765  bnj1519  33766  bnj1520  33767  bnj1525  33770  bnj1523  33772  cvmcov  33944  nfwsuc  34479  nfwlim  34483  nfaltop  34641  currysetlem1  35491  topdifinfindis  35890  rdgssun  35922  exrecfnlem  35923  finxpreclem6  35940  sdclem1  36275  riotasv2s  37493  cdleme26ee  38896  cdlemefs32sn1aw  38950  cdleme43fsv1snlem  38956  cdleme41sn3a  38969  cdleme32d  38980  cdleme32f  38982  cdleme40m  39003  cdleme40n  39004  ltrniotaval  39117  cdlemksv2  39383  cdlemkuv2  39403  cdlemk36  39449  cdlemk38  39451  cdlemkid  39472  cdlemk19x  39479  cdlemk11t  39482  areaquad  41608  nfscott  42641  nfcoll  42658  binomcxplemdvbinom  42755  binomcxplemdvsum  42757  binomcxplemnotnn0  42758  refsum2cnlem1  43364  eliuniincex  43441  disjrnmpt2  43529  fompt  43533  rnmptssbi  43610  allbutfi  43748  allbutfiinf  43775  rexanuz2nf  43848  fmuldfeqlem1  43943  fmuldfeq  43944  mullimc  43977  idlimc  43987  limcperiod  43989  neglimc  44008  addlimc  44009  0ellimcdiv  44010  fnlimcnv  44028  fnlimfvre  44035  fnlimfvre2  44038  fnlimf  44039  fnlimabslt  44040  xlimmnfmpt  44204  xlimpnfmpt  44205  cncfmptssg  44232  cncfshift  44235  cncficcgt0  44249  cncfiooicclem1  44254  dvnmul  44304  dvnprodlem1  44307  itgsinexplem1  44315  itgsubsticclem  44336  stoweidlem14  44375  stoweidlem16  44377  stoweidlem18  44379  stoweidlem22  44383  stoweidlem26  44387  stoweidlem27  44388  stoweidlem31  44392  stoweidlem32  44393  stoweidlem34  44395  stoweidlem35  44396  stoweidlem40  44401  stoweidlem41  44402  stoweidlem42  44403  stoweidlem44  44405  stoweidlem45  44406  stoweidlem46  44407  stoweidlem47  44408  stoweidlem48  44409  stoweidlem50  44411  stoweidlem51  44412  stoweidlem52  44413  stoweidlem53  44414  stoweidlem54  44415  stoweidlem57  44418  stoweidlem59  44420  stoweidlem62  44423  wallispilem5  44430  stirlinglem4  44438  stirlinglem5  44439  stirlinglem8  44442  stirlinglem11  44445  stirlinglem12  44446  stirlinglem13  44447  stirlinglem14  44448  stirlinglem15  44449  fourierdlem20  44488  fourierdlem31  44499  fourierdlem68  44535  fourierdlem80  44547  fourierdlem89  44556  fourierdlem91  44558  fourierdlem103  44570  fourierdlem104  44571  fourierdlem112  44579  fourierdlem115  44582  fourierd  44583  fourierclimd  44584  etransclem48  44643  iundjiun  44821  meaiuninc3v  44845  ovnlerp  44923  ovncvrrp  44925  ovnhoilem1  44962  opnvonmbllem1  44993  iunhoiioolem  45036  vonioo  45043  vonicc  45046  pimdecfgtioc  45076  pimincfltioc  45077  pimdecfgtioo  45078  pimincfltioo  45079  issmff  45095  incsmflem  45102  smfpimltxr  45108  smfconst  45110  decsmflem  45127  smfpreimagtf  45129  smflimlem2  45133  smflim  45138  smfpimgtxr  45141  smfresal  45149  smfmullem2  45153  smfmullem4  45155  smfpimbor1lem2  45160  smflim2  45167  smfpimcclem  45168  smflimmpt  45171  smfsup  45175  smfsupmpt  45176  smfsupxr  45177  smfinf  45179  smfinfmpt  45180  smflimsuplem2  45182  smflimsuplem5  45185  smflimsup  45189  smfliminf  45192  smfpimne2  45201  smfdivdmmbl2  45202  fsupdm  45203  fsupdm2  45204  finfdm  45207  finfdm2  45208  nfafv  45488  nfaov  45531  nfafv2  45570  prmdvdsfmtnof1lem1  45896  nfsetrecs  47251