Theorem nfcxfr 2895

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

Syntax hints:   = wceq 1542  Ⅎwnfc 2882

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-nf 1786  df-cleq 2727  df-clel 2810  df-nfc 2884

This theorem is referenced by:  nfrab1  3418  nfrabw  3435  nfrab  3437  nfdifOLD  4081  nfunOLD  4122  nfinOLD  4176  nfsymdif  4208  nfpw  4572  nfpr  4648  nfsn  4663  nfop  4844  nfint  4911  nfiun  4977  nfiin  4978  nfiung  4979  nfiing  4980  nfiu1OLD  4982  nfii1  4983  nfopab1  5167  nfopab2  5168  nfmpt  5195  nfmpt1  5196  nfxp  5656  nfco  5813  nfcnv  5826  nfdm  5899  nfrn  5900  nfres  5939  nfima  6026  nfpred  6263  nfsuc  6390  nfiota1  6449  nffv  6843  fvmptss  6953  fvmptf  6962  fvopab5  6974  ralrnmptw  7039  ralrnmpt  7041  f1ompt  7056  fompt  7063  f1mpt  7207  fliftfun  7258  nfriota1  7322  riotaprop  7342  nfoprab1  7419  nfoprab2  7420  nfoprab3  7421  nfoprab  7422  nfmpo1  7438  nfmpo2  7439  nfmpo  7440  ovmpos  7506  ov2gf  7507  ov3  7521  nfof  7628  nfofr  7629  nftpos  8203  fvmpocurryd  8213  nffrecs  8225  nfwrecs  8256  nfrecs  8306  nfrdg  8345  rdgsucmptf  8359  rdgsucmptnf  8360  frsucmpt  8369  frsucmptn  8370  nfixpw  8856  nfixp  8857  nfixp1  8858  xpcomco  8997  nfsup  9356  nfinf  9388  nfoi  9421  cnfcom3clem  9616  ttrclselem1  9636  ttrclselem2  9637  nfdju  9821  dfac8clem  9944  iunfo  10451  pwfseqlem2  10572  pwfseqlem4a  10574  pwfseqlem4  10575  reclem2pr  10961  nfseq  13936  nfwrd  14468  nfsum1  15615  nfsum  15616  nfcprod1  15833  nfcprod  15834  symgval  19302  ptbasfi  23527  mbfsup  25623  itg1climres  25673  itg2splitlem  25707  itg2split  25708  nfitg1  25733  nfitg  25734  lgamgulm2  27004  lgseisenlem2  27345  nosupbnd2  27686  noinfbnd2  27701  nfseqs  28266  lfgrnloop  29179  numclwlk2lem2f1o  30435  cnlnadjlem5  32127  2ndresdju  32707  nfesum1  34176  nfesum2  34177  ballotlem7  34672  bnj1230  34937  bnj1476  34982  bnj900  35064  bnj958  35075  bnj1000  35076  bnj1014  35096  bnj1123  35121  bnj1307  35158  bnj1321  35162  bnj1384  35167  bnj1398  35169  bnj1408  35171  bnj1444  35178  bnj1445  35179  bnj1446  35180  bnj1447  35181  bnj1448  35182  bnj1449  35183  bnj1466  35188  bnj1467  35189  bnj1518  35199  bnj1519  35200  bnj1520  35201  bnj1525  35204  bnj1523  35206  cvmcov  35436  nfwsuc  35989  nfwlim  35993  nfaltop  36153  currysetlem1  37121  topdifinfindis  37520  rdgssun  37552  exrecfnlem  37553  finxpreclem6  37570  sdclem1  37913  riotasv2s  39253  cdleme26ee  40655  cdlemefs32sn1aw  40709  cdleme43fsv1snlem  40715  cdleme41sn3a  40728  cdleme32d  40739  cdleme32f  40741  cdleme40m  40762  cdleme40n  40763  ltrniotaval  40876  cdlemksv2  41142  cdlemkuv2  41162  cdlemk36  41208  cdlemk38  41210  cdlemkid  41231  cdlemk19x  41238  cdlemk11t  41241  areaquad  43495  nfscott  44517  nfcoll  44534  binomcxplemdvbinom  44631  binomcxplemdvsum  44633  binomcxplemnotnn0  44634  refsum2cnlem1  45319  eliuniincex  45390  disjrnmpt2  45469  rnmptssbi  45541  allbutfi  45674  allbutfiinf  45701  rexanuz2nf  45773  fmuldfeqlem1  45865  fmuldfeq  45866  mullimc  45899  idlimc  45909  limcperiod  45911  neglimc  45928  addlimc  45929  0ellimcdiv  45930  fnlimcnv  45948  fnlimfvre  45955  fnlimfvre2  45958  fnlimf  45959  fnlimabslt  45960  xlimmnfmpt  46124  xlimpnfmpt  46125  cncfmptssg  46152  cncfshift  46155  cncficcgt0  46169  cncfiooicclem1  46174  dvnmul  46224  dvnprodlem1  46227  itgsinexplem1  46235  itgsubsticclem  46256  stoweidlem14  46295  stoweidlem16  46297  stoweidlem18  46299  stoweidlem22  46303  stoweidlem26  46307  stoweidlem27  46308  stoweidlem31  46312  stoweidlem32  46313  stoweidlem34  46315  stoweidlem35  46316  stoweidlem40  46321  stoweidlem41  46322  stoweidlem42  46323  stoweidlem44  46325  stoweidlem45  46326  stoweidlem46  46327  stoweidlem47  46328  stoweidlem48  46329  stoweidlem50  46331  stoweidlem51  46332  stoweidlem52  46333  stoweidlem53  46334  stoweidlem54  46335  stoweidlem57  46338  stoweidlem59  46340  stoweidlem62  46343  wallispilem5  46350  stirlinglem4  46358  stirlinglem5  46359  stirlinglem8  46362  stirlinglem11  46365  stirlinglem12  46366  stirlinglem13  46367  stirlinglem14  46368  stirlinglem15  46369  fourierdlem20  46408  fourierdlem31  46419  fourierdlem68  46455  fourierdlem80  46467  fourierdlem89  46476  fourierdlem91  46478  fourierdlem103  46490  fourierdlem104  46491  fourierdlem112  46499  fourierdlem115  46502  fourierd  46503  fourierclimd  46504  etransclem48  46563  iundjiun  46741  meaiuninc3v  46765  ovnlerp  46843  ovncvrrp  46845  ovnhoilem1  46882  opnvonmbllem1  46913  iunhoiioolem  46956  vonioo  46963  vonicc  46966  pimdecfgtioc  46996  pimincfltioc  46997  pimdecfgtioo  46998  pimincfltioo  46999  issmff  47015  incsmflem  47022  smfpimltxr  47028  smfconst  47030  decsmflem  47047  smfpreimagtf  47049  smflimlem2  47053  smflim  47058  smfpimgtxr  47061  smfresal  47069  smfmullem2  47073  smfmullem4  47075  smfpimbor1lem2  47080  smflim2  47087  smfpimcclem  47088  smflimmpt  47091  smfsup  47095  smfsupmpt  47096  smfsupxr  47097  smfinf  47099  smfinfmpt  47100  smflimsuplem2  47102  smflimsuplem5  47105  smflimsup  47109  smfliminf  47112  smfpimne2  47121  smfdivdmmbl2  47122  fsupdm  47123  fsupdm2  47124  finfdm  47127  finfdm2  47128  nfafv  47419  nfaov  47462  nfafv2  47501  prmdvdsfmtnof1lem1  47867  nfsetrecs  49968