Theorem nfcxfr 2345

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

Syntax hints:   = wceq 1373  Ⅎwnfc 2335

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-cleq 2198  df-clel 2201  df-nfc 2337

This theorem is referenced by:  nfrab1  2686  nfrabw  2687  nfdif  3294  nfun  3329  nfin  3379  nfpw  3629  nfpr  3683  nfsn  3693  nfop  3835  nfuni  3856  nfint  3895  nfiunxy  3953  nfiinxy  3954  nfiunya  3955  nfiinya  3956  nfiu1  3957  nfii1  3958  nfopab  4112  nfopab1  4113  nfopab2  4114  nfmpt  4136  nfmpt1  4137  repizf2  4206  nfsuc  4455  nfxp  4702  nfco  4843  nfcnv  4857  nfdm  4922  nfrn  4923  nfres  4961  nfima  5030  nfiota1  5234  nffv  5586  fvmptss2  5654  fvmptssdm  5664  fvmptf  5672  ralrnmpt  5722  rexrnmpt  5723  f1ompt  5731  f1mpt  5840  fliftfun  5865  nfriota1  5907  riotaprop  5923  nfoprab1  5994  nfoprab2  5995  nfoprab3  5996  nfoprab  5997  nfmpo1  6012  nfmpo2  6013  nfmpo  6014  ovmpos  6069  ov2gf  6070  ovi3  6083  nfof  6164  nfofr  6165  nftpos  6365  nfrecs  6393  nffrec  6482  nfixpxy  6804  nfixp1  6805  xpcomco  6921  nfsup  7094  nfinf  7119  nfdju  7144  caucvgprprlemaddq  7821  nfseq  10602  nfwrd  11022  nfsum1  11667  nfsum  11668  nfcprod1  11865  nfcprod  11866  lgseisenlem2  15548