Theorem nfcxfr 2902

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

Syntax hints:   = wceq 1543  Ⅎwnfc 2884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-nf 1792  df-cleq 2729  df-clel 2816  df-nfc 2886

This theorem is referenced by:  nfrab1  3296  nfrabw  3297  nfrab  3298  nfdif  4040  nfun  4079  nfin  4131  nfsymdif  4161  nfpw  4534  nfpr  4606  nfsn  4623  nfop  4800  nfint  4869  nfiun  4934  nfiin  4935  nfiung  4936  nfiing  4937  nfiu1  4938  nfii1  4939  nfopab1  5123  nfopab2  5124  nfmpt  5152  nfmpt1  5153  nfxp  5584  nfco  5734  nfcnv  5747  nfdm  5820  nfrn  5821  nfres  5853  nfima  5937  nfpred  6165  nfsuc  6284  nfiota1  6340  nffv  6727  fvmptss  6830  fvmptf  6839  fvopab5  6850  ralrnmptw  6913  ralrnmpt  6915  f1ompt  6928  f1mpt  7073  fliftfun  7121  nfriota1  7177  riotaprop  7198  nfoprab1  7272  nfoprab2  7273  nfoprab3  7274  nfoprab  7275  nfmpo1  7291  nfmpo2  7292  nfmpo  7293  ovmpos  7357  ov2gf  7358  ov3  7371  nfof  7474  nfofr  7475  nftpos  8003  fvmpocurryd  8013  nffrecs  8025  nfwrecs  8049  nfrecs  8111  nfrdg  8150  rdgsucmptf  8164  rdgsucmptnf  8165  frsucmpt  8173  frsucmptn  8174  nfixpw  8597  nfixp  8598  nfixp1  8599  xpcomco  8735  nfsup  9067  nfinf  9098  nfoi  9130  cnfcom3clem  9320  nfdju  9523  dfac8clem  9646  iunfo  10153  pwfseqlem2  10273  pwfseqlem4a  10275  pwfseqlem4  10276  reclem2pr  10662  nfseq  13584  nfwrd  14098  nfsum1  15253  nfsum  15254  nfsumOLD  15255  nfcprod1  15472  nfcprod  15473  symgval  18761  ptbasfi  22478  mbfsup  24561  itg1climres  24612  itg2splitlem  24646  itg2split  24647  nfitg1  24671  nfitg  24672  lgamgulm2  25918  lgseisenlem2  26257  lfgrnloop  27216  numclwlk2lem2f1o  28462  cnlnadjlem5  30152  2ndresdju  30705  nfesum1  31720  nfesum2  31721  ballotlem7  32214  bnj1230  32495  bnj1476  32540  bnj900  32622  bnj958  32633  bnj1000  32634  bnj1014  32654  bnj1123  32679  bnj1307  32716  bnj1321  32720  bnj1384  32725  bnj1398  32727  bnj1408  32729  bnj1444  32736  bnj1445  32737  bnj1446  32738  bnj1447  32739  bnj1448  32740  bnj1449  32741  bnj1466  32746  bnj1467  32747  bnj1518  32757  bnj1519  32758  bnj1520  32759  bnj1525  32762  bnj1523  32764  cvmcov  32938  nfwsuc  33549  nfwlim  33553  nosupbnd2  33656  noinfbnd2  33671  nfaltop  34019  currysetlem1  34873  topdifinfindis  35254  rdgssun  35286  exrecfnlem  35287  finxpreclem6  35304  sdclem1  35638  riotasv2s  36709  cdleme26ee  38111  cdlemefs32sn1aw  38165  cdleme43fsv1snlem  38171  cdleme41sn3a  38184  cdleme32d  38195  cdleme32f  38197  cdleme40m  38218  cdleme40n  38219  ltrniotaval  38332  cdlemksv2  38598  cdlemkuv2  38618  cdlemk36  38664  cdlemk38  38666  cdlemkid  38687  cdlemk19x  38694  cdlemk11t  38697  areaquad  40750  nfscott  41530  nfcoll  41547  binomcxplemdvbinom  41644  binomcxplemdvsum  41646  binomcxplemnotnn0  41647  refsum2cnlem1  42253  eliuniincex  42332  disjrnmpt2  42399  fompt  42403  rnmptssbi  42479  allbutfi  42606  allbutfiinf  42633  fmuldfeqlem1  42798  fmuldfeq  42799  mullimc  42832  idlimc  42842  limcperiod  42844  neglimc  42863  addlimc  42864  0ellimcdiv  42865  fnlimcnv  42883  fnlimfvre  42890  fnlimfvre2  42893  fnlimf  42894  fnlimabslt  42895  xlimmnfmpt  43059  xlimpnfmpt  43060  cncfmptssg  43087  cncfshift  43090  cncficcgt0  43104  cncfiooicclem1  43109  dvnmul  43159  dvnprodlem1  43162  itgsinexplem1  43170  itgsubsticclem  43191  stoweidlem14  43230  stoweidlem16  43232  stoweidlem18  43234  stoweidlem22  43238  stoweidlem26  43242  stoweidlem27  43243  stoweidlem31  43247  stoweidlem32  43248  stoweidlem34  43250  stoweidlem35  43251  stoweidlem40  43256  stoweidlem41  43257  stoweidlem42  43258  stoweidlem44  43260  stoweidlem45  43261  stoweidlem46  43262  stoweidlem47  43263  stoweidlem48  43264  stoweidlem50  43266  stoweidlem51  43267  stoweidlem52  43268  stoweidlem53  43269  stoweidlem54  43270  stoweidlem57  43273  stoweidlem59  43275  stoweidlem62  43278  wallispilem5  43285  stirlinglem4  43293  stirlinglem5  43294  stirlinglem8  43297  stirlinglem11  43300  stirlinglem12  43301  stirlinglem13  43302  stirlinglem14  43303  stirlinglem15  43304  fourierdlem20  43343  fourierdlem31  43354  fourierdlem68  43390  fourierdlem80  43402  fourierdlem89  43411  fourierdlem91  43413  fourierdlem103  43425  fourierdlem104  43426  fourierdlem112  43434  fourierdlem115  43437  fourierd  43438  fourierclimd  43439  etransclem48  43498  iundjiun  43673  meaiuninc3v  43697  ovnlerp  43775  ovncvrrp  43777  ovnhoilem1  43814  opnvonmbllem1  43845  iunhoiioolem  43888  vonioo  43895  vonicc  43898  pimdecfgtioc  43924  pimincfltioc  43925  pimdecfgtioo  43926  pimincfltioo  43927  issmff  43942  incsmflem  43949  smfconst  43957  decsmflem  43973  smfpreimagtf  43975  smflimlem2  43979  smflim  43984  smfpimgtxr  43987  smfresal  43994  smfmullem2  43998  smfmullem4  44000  smfpimbor1lem2  44005  smflim2  44011  smfpimcclem  44012  smflimmpt  44015  smfsup  44019  smfsupmpt  44020  smfsupxr  44021  smfinf  44023  smfinfmpt  44024  smflimsuplem2  44026  smflimsuplem5  44029  smflimsup  44033  smfliminf  44036  nfafv  44300  nfaov  44343  nfafv2  44382  prmdvdsfmtnof1lem1  44709  nfsetrecs  46063