Theorem nfcxfr 2371

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

Syntax hints:   = wceq 1397  Ⅎwnfc 2361

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213

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

This theorem is referenced by:  nfrab1  2713  nfrabw  2714  nfdif  3328  nfun  3363  nfin  3413  nfpw  3665  nfpr  3719  nfsn  3729  nfop  3878  nfuni  3899  nfint  3938  nfiunxy  3996  nfiinxy  3997  nfiunya  3998  nfiinya  3999  nfiu1  4000  nfii1  4001  nfopab  4157  nfopab1  4158  nfopab2  4159  nfmpt  4181  nfmpt1  4182  repizf2  4252  nfsuc  4505  nfxp  4752  nfco  4895  nfcnv  4909  nfdm  4976  nfrn  4977  nfres  5015  nfima  5084  nfiota1  5288  nffv  5649  fvmptss2  5721  fvmptssdm  5731  fvmptf  5739  ralrnmpt  5789  rexrnmpt  5790  f1ompt  5798  f1mpt  5911  fliftfun  5936  nfriota1  5978  riotaprop  5996  nfoprab1  6069  nfoprab2  6070  nfoprab3  6071  nfoprab  6072  nfmpo1  6087  nfmpo2  6088  nfmpo  6089  ovmpos  6144  ov2gf  6145  ovi3  6158  nfof  6240  nfofr  6241  nftpos  6444  nfrecs  6472  nffrec  6561  nfixpxy  6885  nfixp1  6886  xpcomco  7009  nfsup  7190  nfinf  7215  nfdju  7240  caucvgprprlemaddq  7927  nfseq  10718  nfwrd  11141  nfsum1  11916  nfsum  11917  nfcprod1  12114  nfcprod  12115  lgseisenlem2  15799  lfgrnloopen  15983