Theorem nfcxfr 2890

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

Syntax hints:   = wceq 1540  Ⅎwnfc 2877

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-cleq 2722  df-clel 2804  df-nfc 2879

This theorem is referenced by:  nfrab1  3429  nfrabw  3446  nfrab  3448  nfdifOLD  4096  nfunOLD  4137  nfinOLD  4191  nfsymdif  4223  nfpw  4585  nfpr  4659  nfsn  4674  nfop  4856  nfint  4923  nfiun  4990  nfiin  4991  nfiung  4992  nfiing  4993  nfiu1OLD  4995  nfii1  4996  nfopab1  5180  nfopab2  5181  nfmpt  5208  nfmpt1  5209  nfxp  5674  nfco  5832  nfcnv  5845  nfdm  5918  nfrn  5919  nfres  5955  nfima  6042  nfpred  6282  nfsuc  6409  nfiota1  6469  nffv  6871  fvmptss  6983  fvmptf  6992  fvopab5  7004  ralrnmptw  7069  ralrnmpt  7071  f1ompt  7086  fompt  7093  f1mpt  7239  fliftfun  7290  nfriota1  7354  riotaprop  7374  nfoprab1  7453  nfoprab2  7454  nfoprab3  7455  nfoprab  7456  nfmpo1  7472  nfmpo2  7473  nfmpo  7474  ovmpos  7540  ov2gf  7541  ov3  7555  nfof  7662  nfofr  7663  nftpos  8243  fvmpocurryd  8253  nffrecs  8265  nfwrecs  8296  nfrecs  8346  nfrdg  8385  rdgsucmptf  8399  rdgsucmptnf  8400  frsucmpt  8409  frsucmptn  8410  nfixpw  8892  nfixp  8893  nfixp1  8894  xpcomco  9036  nfsup  9409  nfinf  9441  nfoi  9474  cnfcom3clem  9665  ttrclselem1  9685  ttrclselem2  9686  nfdju  9867  dfac8clem  9992  iunfo  10499  pwfseqlem2  10619  pwfseqlem4a  10621  pwfseqlem4  10622  reclem2pr  11008  nfseq  13983  nfwrd  14515  nfsum1  15663  nfsum  15664  nfcprod1  15881  nfcprod  15882  symgval  19308  ptbasfi  23475  mbfsup  25572  itg1climres  25622  itg2splitlem  25656  itg2split  25657  nfitg1  25682  nfitg  25683  lgamgulm2  26953  lgseisenlem2  27294  nosupbnd2  27635  noinfbnd2  27650  nfseqs  28188  lfgrnloop  29059  numclwlk2lem2f1o  30315  cnlnadjlem5  32007  2ndresdju  32580  nfesum1  34037  nfesum2  34038  ballotlem7  34534  bnj1230  34799  bnj1476  34844  bnj900  34926  bnj958  34937  bnj1000  34938  bnj1014  34958  bnj1123  34983  bnj1307  35020  bnj1321  35024  bnj1384  35029  bnj1398  35031  bnj1408  35033  bnj1444  35040  bnj1445  35041  bnj1446  35042  bnj1447  35043  bnj1448  35044  bnj1449  35045  bnj1466  35050  bnj1467  35051  bnj1518  35061  bnj1519  35062  bnj1520  35063  bnj1525  35066  bnj1523  35068  cvmcov  35257  nfwsuc  35813  nfwlim  35817  nfaltop  35975  currysetlem1  36942  topdifinfindis  37341  rdgssun  37373  exrecfnlem  37374  finxpreclem6  37391  sdclem1  37744  riotasv2s  38958  cdleme26ee  40361  cdlemefs32sn1aw  40415  cdleme43fsv1snlem  40421  cdleme41sn3a  40434  cdleme32d  40445  cdleme32f  40447  cdleme40m  40468  cdleme40n  40469  ltrniotaval  40582  cdlemksv2  40848  cdlemkuv2  40868  cdlemk36  40914  cdlemk38  40916  cdlemkid  40937  cdlemk19x  40944  cdlemk11t  40947  areaquad  43212  nfscott  44235  nfcoll  44252  binomcxplemdvbinom  44349  binomcxplemdvsum  44351  binomcxplemnotnn0  44352  refsum2cnlem1  45038  eliuniincex  45110  disjrnmpt2  45189  rnmptssbi  45261  allbutfi  45396  allbutfiinf  45423  rexanuz2nf  45495  fmuldfeqlem1  45587  fmuldfeq  45588  mullimc  45621  idlimc  45631  limcperiod  45633  neglimc  45652  addlimc  45653  0ellimcdiv  45654  fnlimcnv  45672  fnlimfvre  45679  fnlimfvre2  45682  fnlimf  45683  fnlimabslt  45684  xlimmnfmpt  45848  xlimpnfmpt  45849  cncfmptssg  45876  cncfshift  45879  cncficcgt0  45893  cncfiooicclem1  45898  dvnmul  45948  dvnprodlem1  45951  itgsinexplem1  45959  itgsubsticclem  45980  stoweidlem14  46019  stoweidlem16  46021  stoweidlem18  46023  stoweidlem22  46027  stoweidlem26  46031  stoweidlem27  46032  stoweidlem31  46036  stoweidlem32  46037  stoweidlem34  46039  stoweidlem35  46040  stoweidlem40  46045  stoweidlem41  46046  stoweidlem42  46047  stoweidlem44  46049  stoweidlem45  46050  stoweidlem46  46051  stoweidlem47  46052  stoweidlem48  46053  stoweidlem50  46055  stoweidlem51  46056  stoweidlem52  46057  stoweidlem53  46058  stoweidlem54  46059  stoweidlem57  46062  stoweidlem59  46064  stoweidlem62  46067  wallispilem5  46074  stirlinglem4  46082  stirlinglem5  46083  stirlinglem8  46086  stirlinglem11  46089  stirlinglem12  46090  stirlinglem13  46091  stirlinglem14  46092  stirlinglem15  46093  fourierdlem20  46132  fourierdlem31  46143  fourierdlem68  46179  fourierdlem80  46191  fourierdlem89  46200  fourierdlem91  46202  fourierdlem103  46214  fourierdlem104  46215  fourierdlem112  46223  fourierdlem115  46226  fourierd  46227  fourierclimd  46228  etransclem48  46287  iundjiun  46465  meaiuninc3v  46489  ovnlerp  46567  ovncvrrp  46569  ovnhoilem1  46606  opnvonmbllem1  46637  iunhoiioolem  46680  vonioo  46687  vonicc  46690  pimdecfgtioc  46720  pimincfltioc  46721  pimdecfgtioo  46722  pimincfltioo  46723  issmff  46739  incsmflem  46746  smfpimltxr  46752  smfconst  46754  decsmflem  46771  smfpreimagtf  46773  smflimlem2  46777  smflim  46782  smfpimgtxr  46785  smfresal  46793  smfmullem2  46797  smfmullem4  46799  smfpimbor1lem2  46804  smflim2  46811  smfpimcclem  46812  smflimmpt  46815  smfsup  46819  smfsupmpt  46820  smfsupxr  46821  smfinf  46823  smfinfmpt  46824  smflimsuplem2  46826  smflimsuplem5  46829  smflimsup  46833  smfliminf  46836  smfpimne2  46845  smfdivdmmbl2  46846  fsupdm  46847  fsupdm2  46848  finfdm  46851  finfdm2  46852  nfafv  47141  nfaov  47184  nfafv2  47223  prmdvdsfmtnof1lem1  47589  nfsetrecs  49679