Theorem nfcxfrd 2900

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

Syntax hints:   → wi 4   = wceq 1547  Ⅎwnfc 2886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-nf 1791  df-cleq 2731  df-clel 2814  df-nfc 2888

This theorem is referenced by:  nfcsb1d  3853  nfcsbd  3856  nfcsbw  3857  nfifd  4484  nfunid  4844  nfopabd  5140  nfiotadw  6444  nfiotad  6446  nfriotadw  7321  nfriotad  7324  nfovd  7385  nfttrcld  9622  nfnegd  11379  nfchnd  18568  nfxnegd  45884  nfintd  50163  nfiund  50164  nfiundg  50165