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

Syntax hints:   = wceq 1539  Ⅎwnfc 2888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-nf 1787  df-cleq 2731  df-clel 2817  df-nfc 2890

This theorem is referenced by:  nfrab1  3318  nfrabw  3319  nfrabwOLD  3320  nfrab  3321  nfdif  4061  nfun  4100  nfin  4151  nfsymdif  4181  nfpw  4555  nfpr  4627  nfsn  4644  nfop  4821  nfint  4890  nfiun  4955  nfiin  4956  nfiung  4957  nfiing  4958  nfiu1  4959  nfii1  4960  nfopab1  5145  nfopab2  5146  nfmpt  5182  nfmpt1  5183  nfxp  5623  nfco  5777  nfcnv  5790  nfdm  5863  nfrn  5864  nfres  5896  nfima  5980  nfpred  6211  nfsuc  6341  nfiota1  6397  nffv  6793  fvmptss  6896  fvmptf  6905  fvopab5  6916  ralrnmptw  6979  ralrnmpt  6981  f1ompt  6994  f1mpt  7143  fliftfun  7192  nfriota1  7248  riotaprop  7269  nfoprab1  7345  nfoprab2  7346  nfoprab3  7347  nfoprab  7348  nfmpo1  7364  nfmpo2  7365  nfmpo  7366  ovmpos  7430  ov2gf  7431  ov3  7444  nfof  7548  nfofr  7549  nftpos  8086  fvmpocurryd  8096  nffrecs  8108  nfwrecs  8141  nfwrecsOLD  8142  nfrecs  8215  nfrdg  8254  rdgsucmptf  8268  rdgsucmptnf  8269  frsucmpt  8278  frsucmptn  8279  nfixpw  8713  nfixp  8714  nfixp1  8715  xpcomco  8858  nfsup  9219  nfinf  9250  nfoi  9282  cnfcom3clem  9472  ttrclselem1  9492  ttrclselem2  9493  nfdju  9674  dfac8clem  9797  iunfo  10304  pwfseqlem2  10424  pwfseqlem4a  10426  pwfseqlem4  10427  reclem2pr  10813  nfseq  13740  nfwrd  14255  nfsum1  15410  nfsum  15411  nfsumOLD  15412  nfcprod1  15629  nfcprod  15630  symgval  18985  ptbasfi  22741  mbfsup  24837  itg1climres  24888  itg2splitlem  24922  itg2split  24923  nfitg1  24947  nfitg  24948  lgamgulm2  26194  lgseisenlem2  26533  lfgrnloop  27504  numclwlk2lem2f1o  28752  cnlnadjlem5  30442  2ndresdju  30995  nfesum1  32017  nfesum2  32018  ballotlem7  32511  bnj1230  32791  bnj1476  32836  bnj900  32918  bnj958  32929  bnj1000  32930  bnj1014  32950  bnj1123  32975  bnj1307  33012  bnj1321  33016  bnj1384  33021  bnj1398  33023  bnj1408  33025  bnj1444  33032  bnj1445  33033  bnj1446  33034  bnj1447  33035  bnj1448  33036  bnj1449  33037  bnj1466  33042  bnj1467  33043  bnj1518  33053  bnj1519  33054  bnj1520  33055  bnj1525  33058  bnj1523  33060  cvmcov  33234  nfwsuc  33821  nfwlim  33825  nosupbnd2  33928  noinfbnd2  33943  nfaltop  34291  currysetlem1  35145  topdifinfindis  35526  rdgssun  35558  exrecfnlem  35559  finxpreclem6  35576  sdclem1  35910  riotasv2s  36979  cdleme26ee  38381  cdlemefs32sn1aw  38435  cdleme43fsv1snlem  38441  cdleme41sn3a  38454  cdleme32d  38465  cdleme32f  38467  cdleme40m  38488  cdleme40n  38489  ltrniotaval  38602  cdlemksv2  38868  cdlemkuv2  38888  cdlemk36  38934  cdlemk38  38936  cdlemkid  38957  cdlemk19x  38964  cdlemk11t  38967  areaquad  41054  nfscott  41864  nfcoll  41881  binomcxplemdvbinom  41978  binomcxplemdvsum  41980  binomcxplemnotnn0  41981  refsum2cnlem1  42587  eliuniincex  42666  disjrnmpt2  42733  fompt  42737  rnmptssbi  42814  allbutfi  42940  allbutfiinf  42967  fmuldfeqlem1  43130  fmuldfeq  43131  mullimc  43164  idlimc  43174  limcperiod  43176  neglimc  43195  addlimc  43196  0ellimcdiv  43197  fnlimcnv  43215  fnlimfvre  43222  fnlimfvre2  43225  fnlimf  43226  fnlimabslt  43227  xlimmnfmpt  43391  xlimpnfmpt  43392  cncfmptssg  43419  cncfshift  43422  cncficcgt0  43436  cncfiooicclem1  43441  dvnmul  43491  dvnprodlem1  43494  itgsinexplem1  43502  itgsubsticclem  43523  stoweidlem14  43562  stoweidlem16  43564  stoweidlem18  43566  stoweidlem22  43570  stoweidlem26  43574  stoweidlem27  43575  stoweidlem31  43579  stoweidlem32  43580  stoweidlem34  43582  stoweidlem35  43583  stoweidlem40  43588  stoweidlem41  43589  stoweidlem42  43590  stoweidlem44  43592  stoweidlem45  43593  stoweidlem46  43594  stoweidlem47  43595  stoweidlem48  43596  stoweidlem50  43598  stoweidlem51  43599  stoweidlem52  43600  stoweidlem53  43601  stoweidlem54  43602  stoweidlem57  43605  stoweidlem59  43607  stoweidlem62  43610  wallispilem5  43617  stirlinglem4  43625  stirlinglem5  43626  stirlinglem8  43629  stirlinglem11  43632  stirlinglem12  43633  stirlinglem13  43634  stirlinglem14  43635  stirlinglem15  43636  fourierdlem20  43675  fourierdlem31  43686  fourierdlem68  43722  fourierdlem80  43734  fourierdlem89  43743  fourierdlem91  43745  fourierdlem103  43757  fourierdlem104  43758  fourierdlem112  43766  fourierdlem115  43769  fourierd  43770  fourierclimd  43771  etransclem48  43830  iundjiun  44005  meaiuninc3v  44029  ovnlerp  44107  ovncvrrp  44109  ovnhoilem1  44146  opnvonmbllem1  44177  iunhoiioolem  44220  vonioo  44227  vonicc  44230  pimdecfgtioc  44260  pimincfltioc  44261  pimdecfgtioo  44262  pimincfltioo  44263  issmff  44279  incsmflem  44286  smfpimltxr  44292  smfconst  44294  decsmflem  44311  smfpreimagtf  44313  smflimlem2  44317  smflim  44322  smfpimgtxr  44325  smfresal  44333  smfmullem2  44337  smfmullem4  44339  smfpimbor1lem2  44344  smflim2  44350  smfpimcclem  44351  smflimmpt  44354  smfsup  44358  smfsupmpt  44359  smfsupxr  44360  smfinf  44362  smfinfmpt  44363  smflimsuplem2  44365  smflimsuplem5  44368  smflimsup  44372  smfliminf  44375  nfafv  44639  nfaov  44682  nfafv2  44721  prmdvdsfmtnof1lem1  45047  nfsetrecs  46403