Theorem nfcxfr 2897

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

Syntax hints:   = wceq 1542  Ⅎwnfc 2884

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-nf 1786  df-cleq 2729  df-clel 2812  df-nfc 2886

This theorem is referenced by:  nfrab1  3420  nfrabw  3437  nfrab  3439  nfdifOLD  4083  nfunOLD  4124  nfinOLD  4178  nfsymdif  4210  nfpw  4574  nfpr  4650  nfsn  4665  nfop  4846  nfint  4913  nfiun  4979  nfiin  4980  nfiung  4981  nfiing  4982  nfiu1OLD  4984  nfii1  4985  nfopab1  5169  nfopab2  5170  nfmpt  5197  nfmpt1  5198  nfxp  5658  nfco  5815  nfcnv  5828  nfdm  5901  nfrn  5902  nfres  5941  nfima  6028  nfpred  6265  nfsuc  6392  nfiota1  6451  nffv  6845  fvmptss  6955  fvmptf  6964  fvopab5  6976  ralrnmptw  7041  ralrnmpt  7043  f1ompt  7058  fompt  7065  f1mpt  7209  fliftfun  7260  nfriota1  7324  riotaprop  7344  nfoprab1  7421  nfoprab2  7422  nfoprab3  7423  nfoprab  7424  nfmpo1  7440  nfmpo2  7441  nfmpo  7442  ovmpos  7508  ov2gf  7509  ov3  7523  nfof  7630  nfofr  7631  nftpos  8205  fvmpocurryd  8215  nffrecs  8227  nfwrecs  8258  nfrecs  8308  nfrdg  8347  rdgsucmptf  8361  rdgsucmptnf  8362  frsucmpt  8371  frsucmptn  8372  nfixpw  8858  nfixp  8859  nfixp1  8860  xpcomco  8999  nfsup  9358  nfinf  9390  nfoi  9423  cnfcom3clem  9618  ttrclselem1  9638  ttrclselem2  9639  nfdju  9823  dfac8clem  9946  iunfo  10453  pwfseqlem2  10574  pwfseqlem4a  10576  pwfseqlem4  10577  reclem2pr  10963  nfseq  13938  nfwrd  14470  nfsum1  15617  nfsum  15618  nfcprod1  15835  nfcprod  15836  symgval  19304  ptbasfi  23529  mbfsup  25625  itg1climres  25675  itg2splitlem  25709  itg2split  25710  nfitg1  25735  nfitg  25736  lgamgulm2  27006  lgseisenlem2  27347  nosupbnd2  27688  noinfbnd2  27703  nfseqs  28287  lfgrnloop  29202  numclwlk2lem2f1o  30458  cnlnadjlem5  32150  2ndresdju  32730  nfesum1  34199  nfesum2  34200  ballotlem7  34695  bnj1230  34960  bnj1476  35005  bnj900  35087  bnj958  35098  bnj1000  35099  bnj1014  35119  bnj1123  35144  bnj1307  35181  bnj1321  35185  bnj1384  35190  bnj1398  35192  bnj1408  35194  bnj1444  35201  bnj1445  35202  bnj1446  35203  bnj1447  35204  bnj1448  35205  bnj1449  35206  bnj1466  35211  bnj1467  35212  bnj1518  35222  bnj1519  35223  bnj1520  35224  bnj1525  35227  bnj1523  35229  cvmcov  35459  nfwsuc  36012  nfwlim  36016  nfaltop  36176  currysetlem1  37150  topdifinfindis  37553  rdgssun  37585  exrecfnlem  37586  finxpreclem6  37603  sdclem1  37946  riotasv2s  39286  cdleme26ee  40688  cdlemefs32sn1aw  40742  cdleme43fsv1snlem  40748  cdleme41sn3a  40761  cdleme32d  40772  cdleme32f  40774  cdleme40m  40795  cdleme40n  40796  ltrniotaval  40909  cdlemksv2  41175  cdlemkuv2  41195  cdlemk36  41241  cdlemk38  41243  cdlemkid  41264  cdlemk19x  41271  cdlemk11t  41274  areaquad  43525  nfscott  44547  nfcoll  44564  binomcxplemdvbinom  44661  binomcxplemdvsum  44663  binomcxplemnotnn0  44664  refsum2cnlem1  45349  eliuniincex  45420  disjrnmpt2  45499  rnmptssbi  45571  allbutfi  45704  allbutfiinf  45731  rexanuz2nf  45803  fmuldfeqlem1  45895  fmuldfeq  45896  mullimc  45929  idlimc  45939  limcperiod  45941  neglimc  45958  addlimc  45959  0ellimcdiv  45960  fnlimcnv  45978  fnlimfvre  45985  fnlimfvre2  45988  fnlimf  45989  fnlimabslt  45990  xlimmnfmpt  46154  xlimpnfmpt  46155  cncfmptssg  46182  cncfshift  46185  cncficcgt0  46199  cncfiooicclem1  46204  dvnmul  46254  dvnprodlem1  46257  itgsinexplem1  46265  itgsubsticclem  46286  stoweidlem14  46325  stoweidlem16  46327  stoweidlem18  46329  stoweidlem22  46333  stoweidlem26  46337  stoweidlem27  46338  stoweidlem31  46342  stoweidlem32  46343  stoweidlem34  46345  stoweidlem35  46346  stoweidlem40  46351  stoweidlem41  46352  stoweidlem42  46353  stoweidlem44  46355  stoweidlem45  46356  stoweidlem46  46357  stoweidlem47  46358  stoweidlem48  46359  stoweidlem50  46361  stoweidlem51  46362  stoweidlem52  46363  stoweidlem53  46364  stoweidlem54  46365  stoweidlem57  46368  stoweidlem59  46370  stoweidlem62  46373  wallispilem5  46380  stirlinglem4  46388  stirlinglem5  46389  stirlinglem8  46392  stirlinglem11  46395  stirlinglem12  46396  stirlinglem13  46397  stirlinglem14  46398  stirlinglem15  46399  fourierdlem20  46438  fourierdlem31  46449  fourierdlem68  46485  fourierdlem80  46497  fourierdlem89  46506  fourierdlem91  46508  fourierdlem103  46520  fourierdlem104  46521  fourierdlem112  46529  fourierdlem115  46532  fourierd  46533  fourierclimd  46534  etransclem48  46593  iundjiun  46771  meaiuninc3v  46795  ovnlerp  46873  ovncvrrp  46875  ovnhoilem1  46912  opnvonmbllem1  46943  iunhoiioolem  46986  vonioo  46993  vonicc  46996  pimdecfgtioc  47026  pimincfltioc  47027  pimdecfgtioo  47028  pimincfltioo  47029  issmff  47045  incsmflem  47052  smfpimltxr  47058  smfconst  47060  decsmflem  47077  smfpreimagtf  47079  smflimlem2  47083  smflim  47088  smfpimgtxr  47091  smfresal  47099  smfmullem2  47103  smfmullem4  47105  smfpimbor1lem2  47110  smflim2  47117  smfpimcclem  47118  smflimmpt  47121  smfsup  47125  smfsupmpt  47126  smfsupxr  47127  smfinf  47129  smfinfmpt  47130  smflimsuplem2  47132  smflimsuplem5  47135  smflimsup  47139  smfliminf  47142  smfpimne2  47151  smfdivdmmbl2  47152  fsupdm  47153  fsupdm2  47154  finfdm  47157  finfdm2  47158  nfafv  47449  nfaov  47492  nfafv2  47531  prmdvdsfmtnof1lem1  47897  nfsetrecs  49998