Theorem nfcxfrd 2902

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

Hypotheses

Ref	Expression
nfcxfr.1	⊢ 𝐴 = 𝐵
nfcxfrd.2	⊢ (𝜑 → Ⅎ𝑥𝐵)

Assertion

Ref	Expression
nfcxfrd	⊢ (𝜑 → Ⅎ𝑥𝐴)

Proof of Theorem nfcxfrd

Step	Hyp	Ref	Expression
1		nfcxfrd.2	. 2 ⊢ (𝜑 → Ⅎ𝑥𝐵)
2		nfcxfr.1	. . 3 ⊢ 𝐴 = 𝐵
3	2	nfceqi 2900	. 2 ⊢ (Ⅎ𝑥𝐴 ↔ Ⅎ𝑥𝐵)
4	1, 3	sylibr 233	1 ⊢ (𝜑 → Ⅎ𝑥𝐴)

Syntax hints:   → wi 4   = wceq 1541  Ⅎwnfc 2883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-nf 1786  df-cleq 2724  df-clel 2810  df-nfc 2885

This theorem is referenced by:  nfcsb1d  3916  nfcsbd  3919  nfcsbw  3920  nfifd  4557  nfunid  4914  nfopabd  5216  nfiotadw  6498  nfiotad  6500  nfriotadw  7372  nfriotad  7376  nfovd  7437  nfttrcld  9704  nfnegd  11454  nfxnegd  44141  nfintd  47708  nfiund  47709  nfiundg  47710