Theorem nfcxfr 2906

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

Syntax hints:   = wceq 1537  Ⅎwnfc 2893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-nf 1782  df-cleq 2732  df-clel 2819  df-nfc 2895

This theorem is referenced by:  nfrab1  3464  nfrabw  3483  nfrabwOLD  3484  nfrab  3486  nfdifOLD  4153  nfunOLD  4194  nfinOLD  4246  nfsymdif  4276  nfpw  4641  nfpr  4715  nfsn  4732  nfop  4913  nfint  4980  nfiun  5046  nfiin  5047  nfiung  5048  nfiing  5049  nfiu1OLD  5051  nfii1  5052  nfopab1  5236  nfopab2  5237  nfmpt  5273  nfmpt1  5274  nfxp  5733  nfco  5890  nfcnv  5903  nfdm  5976  nfrn  5977  nfres  6011  nfima  6097  nfpred  6337  nfsuc  6467  nfiota1  6527  nffv  6930  fvmptss  7041  fvmptf  7050  fvopab5  7062  ralrnmptw  7128  ralrnmpt  7130  f1ompt  7145  fompt  7152  f1mpt  7298  fliftfun  7348  nfriota1  7411  riotaprop  7432  nfoprab1  7511  nfoprab2  7512  nfoprab3  7513  nfoprab  7514  nfmpo1  7530  nfmpo2  7531  nfmpo  7532  ovmpos  7598  ov2gf  7599  ov3  7613  nfof  7720  nfofr  7721  nftpos  8302  fvmpocurryd  8312  nffrecs  8324  nfwrecs  8357  nfwrecsOLD  8358  nfrecs  8431  nfrdg  8470  rdgsucmptf  8484  rdgsucmptnf  8485  frsucmpt  8494  frsucmptn  8495  nfixpw  8974  nfixp  8975  nfixp1  8976  xpcomco  9128  nfsup  9520  nfinf  9551  nfoi  9583  cnfcom3clem  9774  ttrclselem1  9794  ttrclselem2  9795  nfdju  9976  dfac8clem  10101  iunfo  10608  pwfseqlem2  10728  pwfseqlem4a  10730  pwfseqlem4  10731  reclem2pr  11117  nfseq  14062  nfwrd  14591  nfsum1  15738  nfsum  15739  nfcprod1  15956  nfcprod  15957  symgval  19412  ptbasfi  23610  mbfsup  25718  itg1climres  25769  itg2splitlem  25803  itg2split  25804  nfitg1  25829  nfitg  25830  lgamgulm2  27097  lgseisenlem2  27438  nosupbnd2  27779  noinfbnd2  27794  nfseqs  28311  lfgrnloop  29160  numclwlk2lem2f1o  30411  cnlnadjlem5  32103  2ndresdju  32667  nfesum1  34004  nfesum2  34005  ballotlem7  34500  bnj1230  34778  bnj1476  34823  bnj900  34905  bnj958  34916  bnj1000  34917  bnj1014  34937  bnj1123  34962  bnj1307  34999  bnj1321  35003  bnj1384  35008  bnj1398  35010  bnj1408  35012  bnj1444  35019  bnj1445  35020  bnj1446  35021  bnj1447  35022  bnj1448  35023  bnj1449  35024  bnj1466  35029  bnj1467  35030  bnj1518  35040  bnj1519  35041  bnj1520  35042  bnj1525  35045  bnj1523  35047  cvmcov  35231  nfwsuc  35782  nfwlim  35786  nfaltop  35944  currysetlem1  36913  topdifinfindis  37312  rdgssun  37344  exrecfnlem  37345  finxpreclem6  37362  sdclem1  37703  riotasv2s  38914  cdleme26ee  40317  cdlemefs32sn1aw  40371  cdleme43fsv1snlem  40377  cdleme41sn3a  40390  cdleme32d  40401  cdleme32f  40403  cdleme40m  40424  cdleme40n  40425  ltrniotaval  40538  cdlemksv2  40804  cdlemkuv2  40824  cdlemk36  40870  cdlemk38  40872  cdlemkid  40893  cdlemk19x  40900  cdlemk11t  40903  areaquad  43177  nfscott  44208  nfcoll  44225  binomcxplemdvbinom  44322  binomcxplemdvsum  44324  binomcxplemnotnn0  44325  refsum2cnlem1  44937  eliuniincex  45011  disjrnmpt2  45095  rnmptssbi  45170  allbutfi  45308  allbutfiinf  45335  rexanuz2nf  45408  fmuldfeqlem1  45503  fmuldfeq  45504  mullimc  45537  idlimc  45547  limcperiod  45549  neglimc  45568  addlimc  45569  0ellimcdiv  45570  fnlimcnv  45588  fnlimfvre  45595  fnlimfvre2  45598  fnlimf  45599  fnlimabslt  45600  xlimmnfmpt  45764  xlimpnfmpt  45765  cncfmptssg  45792  cncfshift  45795  cncficcgt0  45809  cncfiooicclem1  45814  dvnmul  45864  dvnprodlem1  45867  itgsinexplem1  45875  itgsubsticclem  45896  stoweidlem14  45935  stoweidlem16  45937  stoweidlem18  45939  stoweidlem22  45943  stoweidlem26  45947  stoweidlem27  45948  stoweidlem31  45952  stoweidlem32  45953  stoweidlem34  45955  stoweidlem35  45956  stoweidlem40  45961  stoweidlem41  45962  stoweidlem42  45963  stoweidlem44  45965  stoweidlem45  45966  stoweidlem46  45967  stoweidlem47  45968  stoweidlem48  45969  stoweidlem50  45971  stoweidlem51  45972  stoweidlem52  45973  stoweidlem53  45974  stoweidlem54  45975  stoweidlem57  45978  stoweidlem59  45980  stoweidlem62  45983  wallispilem5  45990  stirlinglem4  45998  stirlinglem5  45999  stirlinglem8  46002  stirlinglem11  46005  stirlinglem12  46006  stirlinglem13  46007  stirlinglem14  46008  stirlinglem15  46009  fourierdlem20  46048  fourierdlem31  46059  fourierdlem68  46095  fourierdlem80  46107  fourierdlem89  46116  fourierdlem91  46118  fourierdlem103  46130  fourierdlem104  46131  fourierdlem112  46139  fourierdlem115  46142  fourierd  46143  fourierclimd  46144  etransclem48  46203  iundjiun  46381  meaiuninc3v  46405  ovnlerp  46483  ovncvrrp  46485  ovnhoilem1  46522  opnvonmbllem1  46553  iunhoiioolem  46596  vonioo  46603  vonicc  46606  pimdecfgtioc  46636  pimincfltioc  46637  pimdecfgtioo  46638  pimincfltioo  46639  issmff  46655  incsmflem  46662  smfpimltxr  46668  smfconst  46670  decsmflem  46687  smfpreimagtf  46689  smflimlem2  46693  smflim  46698  smfpimgtxr  46701  smfresal  46709  smfmullem2  46713  smfmullem4  46715  smfpimbor1lem2  46720  smflim2  46727  smfpimcclem  46728  smflimmpt  46731  smfsup  46735  smfsupmpt  46736  smfsupxr  46737  smfinf  46739  smfinfmpt  46740  smflimsuplem2  46742  smflimsuplem5  46745  smflimsup  46749  smfliminf  46752  smfpimne2  46761  smfdivdmmbl2  46762  fsupdm  46763  fsupdm2  46764  finfdm  46767  finfdm2  46768  nfafv  47051  nfaov  47094  nfafv2  47133  prmdvdsfmtnof1lem1  47458  nfsetrecs  48778