Theorem nfcxfrd 2925

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  Ⅎwnfc 2911

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-nf 1816  df-cleq 2755  df-clel 2839  df-nfc 2913

This theorem is used by:  nfcsb1d  3873  nfcsbd  3876  nfcsbw  3877  nfifd  4515  nfunid  4876  nfopabd  5176  nfiotadw  6504  nfiotad  6506  nfriotadw  7395  nfriotad  7398  nfovd  7459  nfttrcld  9724  nfnegd  11565  nfchnd  18800  nfxnegd  46593  nfintd  50998  nfiund  50999  nfiundg  51000