Theorem nfcxfrd 2979

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 2976	. 2 ⊢ (Ⅎ𝑥𝐴 ↔ Ⅎ𝑥𝐵)
4	1, 3	sylibr 236	1 ⊢ (𝜑 → Ⅎ𝑥𝐴)

Syntax hints:   → wi 4   = wceq 1536  Ⅎwnfc 2964

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-nf 1784  df-cleq 2817  df-clel 2896  df-nfc 2966

This theorem is referenced by:  nfcsb1d  3908  nfcsbd  3911  nfcsbw  3912  nfifd  4498  nfunid  4847  nfiotadw  6320  nfiotad  6322  nfriotadw  7125  nfriotad  7128  nfovd  7188  nfnegd  10884  nfxnegd  41721  nfintd  44783  nfiund  44784  nfiundg  44785