Theorem nfcxfr 2749

Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypotheses

Ref	Expression
nfceqi.1	⊢ 𝐴 = 𝐵
nfcxfr.2	⊢ Ⅎ𝑥𝐵

Assertion

Ref	Expression
nfcxfr	⊢ Ⅎ𝑥𝐴

Proof of Theorem nfcxfr

Step	Hyp	Ref	Expression
1		nfcxfr.2	. 2 ⊢ Ⅎ𝑥𝐵
2		nfceqi.1	. . 3 ⊢ 𝐴 = 𝐵
3	2	nfceqi 2748	. 2 ⊢ (Ⅎ𝑥𝐴 ↔ Ⅎ𝑥𝐵)
4	1, 3	mpbir 220	1 ⊢ Ⅎ𝑥𝐴

Syntax hints:   = wceq 1475  Ⅎwnfc 2738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-cleq 2603  df-clel 2606  df-nfc 2740

This theorem is referenced by:  nfrab1  3099  nfrab  3100  nfdif  3693  nfun  3731  nfin  3782  nfsymdif  3810  nfpw  4120  nfpr  4179  nfsn  4189  nfop  4356  nfuni  4378  nfint  4421  nfiun  4484  nfiin  4485  nfiu1  4486  nfii1  4487  nfopab  4650  nfopab1  4651  nfopab2  4652  nfmpt  4674  nfmpt1  4675  nfxp  5066  nfco  5209  nfcnv  5223  nfdm  5288  nfrn  5289  nfres  5319  nfima  5393  nfpred  5602  nfsuc  5713  nfiota1  5770  nffv  6110  fvmptss  6201  fvmptf  6209  fvopab5  6217  ralrnmpt  6276  f1ompt  6290  f1mpt  6419  fliftfun  6462  nfriota1  6518  riotaprop  6534  nfoprab1  6602  nfoprab2  6603  nfoprab3  6604  nfoprab  6605  nfmpt21  6620  nfmpt22  6621  nfmpt2  6622  ovmpt2s  6682  ov2gf  6683  ov3  6695  nftpos  7274  fvmpt2curryd  7284  nfwrecs  7296  nfrecs  7358  nfrdg  7397  rdgsucmptf  7411  rdgsucmptnf  7412  frsucmpt  7420  frsucmptn  7421  nfixp  7813  nfixp1  7814  xpcomco  7935  nfsup  8240  nfinf  8271  nfoi  8302  cnfcom3clem  8485  dfac8clem  8738  iunfo  9240  pwfseqlem2  9360  pwfseqlem4a  9362  pwfseqlem4  9363  reclem2pr  9749  nfseq  12673  nfwrd  13188  nfsum1  14268  nfsum  14269  nfcprod1  14479  nfcprod  14480  ptbasfi  21194  mbfsup  23237  itg1climres  23287  itg2splitlem  23321  itg2split  23322  nfitg1  23346  nfitg  23347  lgamgulm2  24562  lgseisenlem2  24901  lfgrnloop  25791  cnlnadjlem5  28314  nfesum1  29429  nfesum2  29430  ballotlem7  29924  bnj1230  30127  bnj1476  30171  bnj900  30253  bnj958  30264  bnj1000  30265  bnj1014  30284  bnj1123  30308  bnj1307  30345  bnj1321  30349  bnj1384  30354  bnj1398  30356  bnj1408  30358  bnj1444  30365  bnj1445  30366  bnj1446  30367  bnj1447  30368  bnj1448  30369  bnj1449  30370  bnj1466  30375  bnj1467  30376  bnj1518  30386  bnj1519  30387  bnj1520  30388  bnj1525  30391  bnj1523  30393  cvmcov  30499  nfwsuc  31008  nfwlim  31012  nfaltop  31257  topdifinfindis  32370  finxpreclem6  32409  sdclem1  32709  riotasv2s  33262  cdleme26ee  34666  cdlemefs32sn1aw  34720  cdleme43fsv1snlem  34726  cdleme41sn3a  34739  cdleme32d  34750  cdleme32f  34752  cdleme40m  34773  cdleme40n  34774  ltrniotaval  34887  cdlemksv2  35153  cdlemkuv2  35173  cdlemk36  35219  cdlemk38  35221  cdlemkid  35242  cdlemk19x  35249  cdlemk11t  35252  areaquad  36821  binomcxplemdvbinom  37574  binomcxplemdvsum  37576  binomcxplemnotnn0  37577  refsum2cnlem1  38219  eliuniincex  38323  suprnmpt  38350  wessf1ornlem  38366  disjrnmpt2  38370  fompt  38374  allbutfi  38557  fmuldfeqlem1  38649  fmuldfeq  38650  mullimc  38683  idlimc  38693  limcperiod  38695  neglimc  38714  addlimc  38715  0ellimcdiv  38716  fnlimcnv  38734  fnlimfvre  38741  fnlimfvre2  38744  fnlimf  38745  fnlimabslt  38746  cncfmptssg  38755  cncfshift  38759  cncficcgt0  38774  cncfiooicclem1  38779  dvnmul  38833  dvnprodlem1  38836  itgsinexplem1  38845  itgsubsticclem  38867  stoweidlem14  38907  stoweidlem16  38909  stoweidlem18  38911  stoweidlem22  38915  stoweidlem26  38919  stoweidlem27  38920  stoweidlem31  38924  stoweidlem32  38925  stoweidlem34  38927  stoweidlem35  38928  stoweidlem40  38933  stoweidlem41  38934  stoweidlem42  38935  stoweidlem44  38937  stoweidlem45  38938  stoweidlem46  38939  stoweidlem47  38940  stoweidlem48  38941  stoweidlem50  38943  stoweidlem51  38944  stoweidlem52  38945  stoweidlem53  38946  stoweidlem54  38947  stoweidlem57  38950  stoweidlem59  38952  stoweidlem62  38955  wallispilem5  38962  stirlinglem4  38970  stirlinglem5  38971  stirlinglem8  38974  stirlinglem11  38977  stirlinglem12  38978  stirlinglem13  38979  stirlinglem14  38980  stirlinglem15  38981  fourierdlem20  39020  fourierdlem31  39031  fourierdlem68  39067  fourierdlem80  39079  fourierdlem89  39088  fourierdlem91  39090  fourierdlem103  39102  fourierdlem104  39103  fourierdlem112  39111  fourierdlem115  39114  fourierd  39115  fourierclimd  39116  etransclem48  39175  iundjiun  39353  ovnlerp  39452  ovncvrrp  39454  ovnhoilem1  39491  opnvonmbllem1  39522  iunhoiioolem  39566  vonioo  39573  vonicc  39576  pimdecfgtioc  39602  pimincfltioc  39603  pimdecfgtioo  39604  pimincfltioo  39605  issmff  39620  incsmflem  39628  smfconst  39636  decsmflem  39652  smfpreimagtf  39654  smflimlem2  39658  smflim  39663  smfpimgtxr  39666  smfresal  39673  smfmullem2  39677  smfmullem4  39679  smfpimbor1lem2  39684  nfafv  39865  nfaov  39908  prmdvdsfmtnof1lem1  40034  nfsetrecs  42232