Theorem nfcxfr 2369

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

Syntax hints:   = wceq 1395  Ⅎwnfc 2359

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-cleq 2222  df-clel 2225  df-nfc 2361

This theorem is referenced by:  nfrab1  2711  nfrabw  2712  nfdif  3325  nfun  3360  nfin  3410  nfpw  3662  nfpr  3716  nfsn  3726  nfop  3873  nfuni  3894  nfint  3933  nfiunxy  3991  nfiinxy  3992  nfiunya  3993  nfiinya  3994  nfiu1  3995  nfii1  3996  nfopab  4152  nfopab1  4153  nfopab2  4154  nfmpt  4176  nfmpt1  4177  repizf2  4246  nfsuc  4499  nfxp  4746  nfco  4887  nfcnv  4901  nfdm  4968  nfrn  4969  nfres  5007  nfima  5076  nfiota1  5280  nffv  5637  fvmptss2  5709  fvmptssdm  5719  fvmptf  5727  ralrnmpt  5777  rexrnmpt  5778  f1ompt  5786  f1mpt  5895  fliftfun  5920  nfriota1  5962  riotaprop  5980  nfoprab1  6053  nfoprab2  6054  nfoprab3  6055  nfoprab  6056  nfmpo1  6071  nfmpo2  6072  nfmpo  6073  ovmpos  6128  ov2gf  6129  ovi3  6142  nfof  6224  nfofr  6225  nftpos  6425  nfrecs  6453  nffrec  6542  nfixpxy  6864  nfixp1  6865  xpcomco  6985  nfsup  7159  nfinf  7184  nfdju  7209  caucvgprprlemaddq  7895  nfseq  10679  nfwrd  11100  nfsum1  11867  nfsum  11868  nfcprod1  12065  nfcprod  12066  lgseisenlem2  15750  lfgrnloopen  15931