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 231	1 ⊢ Ⅎ𝑥𝐴

Syntax hints:   = wceq 1536  Ⅎwnfc 2887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-nf 1780  df-cleq 2726  df-clel 2813  df-nfc 2889

This theorem is referenced by:  nfrab1  3453  nfrabw  3472  nfrabwOLD  3473  nfrab  3475  nfdifOLD  4139  nfunOLD  4180  nfinOLD  4232  nfsymdif  4262  nfpw  4623  nfpr  4696  nfsn  4711  nfop  4893  nfint  4960  nfiun  5027  nfiin  5028  nfiung  5029  nfiing  5030  nfiu1OLD  5032  nfii1  5033  nfopab1  5217  nfopab2  5218  nfmpt  5254  nfmpt1  5255  nfxp  5721  nfco  5878  nfcnv  5891  nfdm  5964  nfrn  5965  nfres  6001  nfima  6087  nfpred  6327  nfsuc  6457  nfiota1  6517  nffv  6916  fvmptss  7027  fvmptf  7036  fvopab5  7048  ralrnmptw  7113  ralrnmpt  7115  f1ompt  7130  fompt  7137  f1mpt  7280  fliftfun  7331  nfriota1  7394  riotaprop  7414  nfoprab1  7493  nfoprab2  7494  nfoprab3  7495  nfoprab  7496  nfmpo1  7512  nfmpo2  7513  nfmpo  7514  ovmpos  7580  ov2gf  7581  ov3  7595  nfof  7702  nfofr  7703  nftpos  8284  fvmpocurryd  8294  nffrecs  8306  nfwrecs  8339  nfwrecsOLD  8340  nfrecs  8413  nfrdg  8452  rdgsucmptf  8466  rdgsucmptnf  8467  frsucmpt  8476  frsucmptn  8477  nfixpw  8954  nfixp  8955  nfixp1  8956  xpcomco  9100  nfsup  9488  nfinf  9519  nfoi  9551  cnfcom3clem  9742  ttrclselem1  9762  ttrclselem2  9763  nfdju  9944  dfac8clem  10069  iunfo  10576  pwfseqlem2  10696  pwfseqlem4a  10698  pwfseqlem4  10699  reclem2pr  11085  nfseq  14048  nfwrd  14577  nfsum1  15722  nfsum  15723  nfcprod1  15940  nfcprod  15941  symgval  19402  ptbasfi  23604  mbfsup  25712  itg1climres  25763  itg2splitlem  25797  itg2split  25798  nfitg1  25823  nfitg  25824  lgamgulm2  27093  lgseisenlem2  27434  nosupbnd2  27775  noinfbnd2  27790  nfseqs  28307  lfgrnloop  29156  numclwlk2lem2f1o  30407  cnlnadjlem5  32099  2ndresdju  32665  nfesum1  34020  nfesum2  34021  ballotlem7  34516  bnj1230  34794  bnj1476  34839  bnj900  34921  bnj958  34932  bnj1000  34933  bnj1014  34953  bnj1123  34978  bnj1307  35015  bnj1321  35019  bnj1384  35024  bnj1398  35026  bnj1408  35028  bnj1444  35035  bnj1445  35036  bnj1446  35037  bnj1447  35038  bnj1448  35039  bnj1449  35040  bnj1466  35045  bnj1467  35046  bnj1518  35056  bnj1519  35057  bnj1520  35058  bnj1525  35061  bnj1523  35063  cvmcov  35247  nfwsuc  35799  nfwlim  35803  nfaltop  35961  currysetlem1  36929  topdifinfindis  37328  rdgssun  37360  exrecfnlem  37361  finxpreclem6  37378  sdclem1  37729  riotasv2s  38939  cdleme26ee  40342  cdlemefs32sn1aw  40396  cdleme43fsv1snlem  40402  cdleme41sn3a  40415  cdleme32d  40426  cdleme32f  40428  cdleme40m  40449  cdleme40n  40450  ltrniotaval  40563  cdlemksv2  40829  cdlemkuv2  40849  cdlemk36  40895  cdlemk38  40897  cdlemkid  40918  cdlemk19x  40925  cdlemk11t  40928  areaquad  43204  nfscott  44234  nfcoll  44251  binomcxplemdvbinom  44348  binomcxplemdvsum  44350  binomcxplemnotnn0  44351  refsum2cnlem1  44974  eliuniincex  45048  disjrnmpt2  45130  rnmptssbi  45205  allbutfi  45342  allbutfiinf  45369  rexanuz2nf  45442  fmuldfeqlem1  45537  fmuldfeq  45538  mullimc  45571  idlimc  45581  limcperiod  45583  neglimc  45602  addlimc  45603  0ellimcdiv  45604  fnlimcnv  45622  fnlimfvre  45629  fnlimfvre2  45632  fnlimf  45633  fnlimabslt  45634  xlimmnfmpt  45798  xlimpnfmpt  45799  cncfmptssg  45826  cncfshift  45829  cncficcgt0  45843  cncfiooicclem1  45848  dvnmul  45898  dvnprodlem1  45901  itgsinexplem1  45909  itgsubsticclem  45930  stoweidlem14  45969  stoweidlem16  45971  stoweidlem18  45973  stoweidlem22  45977  stoweidlem26  45981  stoweidlem27  45982  stoweidlem31  45986  stoweidlem32  45987  stoweidlem34  45989  stoweidlem35  45990  stoweidlem40  45995  stoweidlem41  45996  stoweidlem42  45997  stoweidlem44  45999  stoweidlem45  46000  stoweidlem46  46001  stoweidlem47  46002  stoweidlem48  46003  stoweidlem50  46005  stoweidlem51  46006  stoweidlem52  46007  stoweidlem53  46008  stoweidlem54  46009  stoweidlem57  46012  stoweidlem59  46014  stoweidlem62  46017  wallispilem5  46024  stirlinglem4  46032  stirlinglem5  46033  stirlinglem8  46036  stirlinglem11  46039  stirlinglem12  46040  stirlinglem13  46041  stirlinglem14  46042  stirlinglem15  46043  fourierdlem20  46082  fourierdlem31  46093  fourierdlem68  46129  fourierdlem80  46141  fourierdlem89  46150  fourierdlem91  46152  fourierdlem103  46164  fourierdlem104  46165  fourierdlem112  46173  fourierdlem115  46176  fourierd  46177  fourierclimd  46178  etransclem48  46237  iundjiun  46415  meaiuninc3v  46439  ovnlerp  46517  ovncvrrp  46519  ovnhoilem1  46556  opnvonmbllem1  46587  iunhoiioolem  46630  vonioo  46637  vonicc  46640  pimdecfgtioc  46670  pimincfltioc  46671  pimdecfgtioo  46672  pimincfltioo  46673  issmff  46689  incsmflem  46696  smfpimltxr  46702  smfconst  46704  decsmflem  46721  smfpreimagtf  46723  smflimlem2  46727  smflim  46732  smfpimgtxr  46735  smfresal  46743  smfmullem2  46747  smfmullem4  46749  smfpimbor1lem2  46754  smflim2  46761  smfpimcclem  46762  smflimmpt  46765  smfsup  46769  smfsupmpt  46770  smfsupxr  46771  smfinf  46773  smfinfmpt  46774  smflimsuplem2  46776  smflimsuplem5  46779  smflimsup  46783  smfliminf  46786  smfpimne2  46795  smfdivdmmbl2  46796  fsupdm  46797  fsupdm2  46798  finfdm  46801  finfdm2  46802  nfafv  47085  nfaov  47128  nfafv2  47167  prmdvdsfmtnof1lem1  47508  nfsetrecs  48916