Theorem nfcxfrd 2924

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

Syntax hints:   → wi 4   = wceq 1570  Ⅎwnfc 2910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-nf 1814  df-cleq 2755  df-clel 2838  df-nfc 2912

This theorem is referenced by:  nfcsb1d  3875  nfcsbd  3878  nfcsbw  3879  nfifd  4517  nfunid  4878  nfopabd  5179  nfiotadw  6495  nfiotad  6497  nfriotadw  7375  nfriotad  7378  nfovd  7439  nfttrcld  9675  nfnegd  11447  nfchnd  18662  nfxnegd  46175  nfintd  50471  nfiund  50472  nfiundg  50473