Theorem nfcxfr 2892

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

Syntax hints:   = wceq 1541  Ⅎwnfc 2879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-nf 1785  df-cleq 2723  df-clel 2806  df-nfc 2881

This theorem is referenced by:  nfrab1  3415  nfrabw  3432  nfrab  3434  nfdifOLD  4077  nfunOLD  4118  nfinOLD  4172  nfsymdif  4204  nfpw  4566  nfpr  4642  nfsn  4657  nfop  4838  nfint  4905  nfiun  4971  nfiin  4972  nfiung  4973  nfiing  4974  nfiu1OLD  4976  nfii1  4977  nfopab1  5159  nfopab2  5160  nfmpt  5187  nfmpt1  5188  nfxp  5647  nfco  5804  nfcnv  5817  nfdm  5890  nfrn  5891  nfres  5929  nfima  6016  nfpred  6253  nfsuc  6380  nfiota1  6439  nffv  6832  fvmptss  6941  fvmptf  6950  fvopab5  6962  ralrnmptw  7027  ralrnmpt  7029  f1ompt  7044  fompt  7051  f1mpt  7195  fliftfun  7246  nfriota1  7310  riotaprop  7330  nfoprab1  7407  nfoprab2  7408  nfoprab3  7409  nfoprab  7410  nfmpo1  7426  nfmpo2  7427  nfmpo  7428  ovmpos  7494  ov2gf  7495  ov3  7509  nfof  7616  nfofr  7617  nftpos  8191  fvmpocurryd  8201  nffrecs  8213  nfwrecs  8244  nfrecs  8294  nfrdg  8333  rdgsucmptf  8347  rdgsucmptnf  8348  frsucmpt  8357  frsucmptn  8358  nfixpw  8840  nfixp  8841  nfixp1  8842  xpcomco  8980  nfsup  9335  nfinf  9367  nfoi  9400  cnfcom3clem  9595  ttrclselem1  9615  ttrclselem2  9616  nfdju  9800  dfac8clem  9923  iunfo  10430  pwfseqlem2  10550  pwfseqlem4a  10552  pwfseqlem4  10553  reclem2pr  10939  nfseq  13918  nfwrd  14450  nfsum1  15597  nfsum  15598  nfcprod1  15815  nfcprod  15816  symgval  19283  ptbasfi  23496  mbfsup  25592  itg1climres  25642  itg2splitlem  25676  itg2split  25677  nfitg1  25702  nfitg  25703  lgamgulm2  26973  lgseisenlem2  27314  nosupbnd2  27655  noinfbnd2  27670  nfseqs  28217  lfgrnloop  29103  numclwlk2lem2f1o  30359  cnlnadjlem5  32051  2ndresdju  32631  nfesum1  34053  nfesum2  34054  ballotlem7  34549  bnj1230  34814  bnj1476  34859  bnj900  34941  bnj958  34952  bnj1000  34953  bnj1014  34973  bnj1123  34998  bnj1307  35035  bnj1321  35039  bnj1384  35044  bnj1398  35046  bnj1408  35048  bnj1444  35055  bnj1445  35056  bnj1446  35057  bnj1447  35058  bnj1448  35059  bnj1449  35060  bnj1466  35065  bnj1467  35066  bnj1518  35076  bnj1519  35077  bnj1520  35078  bnj1525  35081  bnj1523  35083  cvmcov  35307  nfwsuc  35860  nfwlim  35864  nfaltop  36024  currysetlem1  36991  topdifinfindis  37390  rdgssun  37422  exrecfnlem  37423  finxpreclem6  37440  sdclem1  37782  riotasv2s  39056  cdleme26ee  40458  cdlemefs32sn1aw  40512  cdleme43fsv1snlem  40518  cdleme41sn3a  40531  cdleme32d  40542  cdleme32f  40544  cdleme40m  40565  cdleme40n  40566  ltrniotaval  40679  cdlemksv2  40945  cdlemkuv2  40965  cdlemk36  41011  cdlemk38  41013  cdlemkid  41034  cdlemk19x  41041  cdlemk11t  41044  areaquad  43308  nfscott  44331  nfcoll  44348  binomcxplemdvbinom  44445  binomcxplemdvsum  44447  binomcxplemnotnn0  44448  refsum2cnlem1  45133  eliuniincex  45205  disjrnmpt2  45284  rnmptssbi  45356  allbutfi  45490  allbutfiinf  45517  rexanuz2nf  45589  fmuldfeqlem1  45681  fmuldfeq  45682  mullimc  45715  idlimc  45725  limcperiod  45727  neglimc  45744  addlimc  45745  0ellimcdiv  45746  fnlimcnv  45764  fnlimfvre  45771  fnlimfvre2  45774  fnlimf  45775  fnlimabslt  45776  xlimmnfmpt  45940  xlimpnfmpt  45941  cncfmptssg  45968  cncfshift  45971  cncficcgt0  45985  cncfiooicclem1  45990  dvnmul  46040  dvnprodlem1  46043  itgsinexplem1  46051  itgsubsticclem  46072  stoweidlem14  46111  stoweidlem16  46113  stoweidlem18  46115  stoweidlem22  46119  stoweidlem26  46123  stoweidlem27  46124  stoweidlem31  46128  stoweidlem32  46129  stoweidlem34  46131  stoweidlem35  46132  stoweidlem40  46137  stoweidlem41  46138  stoweidlem42  46139  stoweidlem44  46141  stoweidlem45  46142  stoweidlem46  46143  stoweidlem47  46144  stoweidlem48  46145  stoweidlem50  46147  stoweidlem51  46148  stoweidlem52  46149  stoweidlem53  46150  stoweidlem54  46151  stoweidlem57  46154  stoweidlem59  46156  stoweidlem62  46159  wallispilem5  46166  stirlinglem4  46174  stirlinglem5  46175  stirlinglem8  46178  stirlinglem11  46181  stirlinglem12  46182  stirlinglem13  46183  stirlinglem14  46184  stirlinglem15  46185  fourierdlem20  46224  fourierdlem31  46235  fourierdlem68  46271  fourierdlem80  46283  fourierdlem89  46292  fourierdlem91  46294  fourierdlem103  46306  fourierdlem104  46307  fourierdlem112  46315  fourierdlem115  46318  fourierd  46319  fourierclimd  46320  etransclem48  46379  iundjiun  46557  meaiuninc3v  46581  ovnlerp  46659  ovncvrrp  46661  ovnhoilem1  46698  opnvonmbllem1  46729  iunhoiioolem  46772  vonioo  46779  vonicc  46782  pimdecfgtioc  46812  pimincfltioc  46813  pimdecfgtioo  46814  pimincfltioo  46815  issmff  46831  incsmflem  46838  smfpimltxr  46844  smfconst  46846  decsmflem  46863  smfpreimagtf  46865  smflimlem2  46869  smflim  46874  smfpimgtxr  46877  smfresal  46885  smfmullem2  46889  smfmullem4  46891  smfpimbor1lem2  46896  smflim2  46903  smfpimcclem  46904  smflimmpt  46907  smfsup  46911  smfsupmpt  46912  smfsupxr  46913  smfinf  46915  smfinfmpt  46916  smflimsuplem2  46918  smflimsuplem5  46921  smflimsup  46925  smfliminf  46928  smfpimne2  46937  smfdivdmmbl2  46938  fsupdm  46939  fsupdm2  46940  finfdm  46943  finfdm2  46944  nfafv  47235  nfaov  47278  nfafv2  47317  prmdvdsfmtnof1lem1  47683  nfsetrecs  49786