Theorem nfcxfr 2372

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

Syntax hints:   = wceq 1398  Ⅎwnfc 2362

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-cleq 2224  df-clel 2227  df-nfc 2364

This theorem is referenced by:  nfrab1  2714  nfrabw  2715  nfdif  3330  nfun  3365  nfin  3415  nfpw  3669  nfpr  3723  nfsn  3733  nfop  3883  nfuni  3904  nfint  3943  nfiunxy  4001  nfiinxy  4002  nfiunya  4003  nfiinya  4004  nfiu1  4005  nfii1  4006  nfopab  4162  nfopab1  4163  nfopab2  4164  nfmpt  4186  nfmpt1  4187  repizf2  4258  nfsuc  4511  nfxp  4758  nfco  4901  nfcnv  4915  nfdm  4982  nfrn  4983  nfres  5021  nfima  5090  nfiota1  5295  nffv  5658  fvmptss2  5730  fvmptssdm  5740  fvmptf  5748  ralrnmpt  5797  rexrnmpt  5798  f1ompt  5806  f1mpt  5922  fliftfun  5947  nfriota1  5989  riotaprop  6007  nfoprab1  6080  nfoprab2  6081  nfoprab3  6082  nfoprab  6083  nfmpo1  6098  nfmpo2  6099  nfmpo  6100  ovmpos  6155  ov2gf  6156  ovi3  6169  nfof  6250  nfofr  6251  nftpos  6488  nfrecs  6516  nffrec  6605  nfixpxy  6929  nfixp1  6930  xpcomco  7053  nfsup  7251  nfinf  7276  nfdju  7301  caucvgprprlemaddq  7988  nfseq  10782  nfwrd  11208  nfsum1  11996  nfsum  11997  nfcprod1  12195  nfcprod  12196  lgseisenlem2  15890  lfgrnloopen  16074