Theorem nfxfrd 1850

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

Hypotheses

Ref	Expression
nfbii.1	⊢ (𝜑 ↔ 𝜓)
nfxfrd.2	⊢ (𝜒 → Ⅎ𝑥𝜓)

Assertion

Ref	Expression
nfxfrd	⊢ (𝜒 → Ⅎ𝑥𝜑)

Proof of Theorem nfxfrd

Step	Hyp	Ref	Expression
1		nfxfrd.2	. 2 ⊢ (𝜒 → Ⅎ𝑥𝜓)
2		nfbii.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
3	2	nfbii 1848	. 2 ⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓)
4	1, 3	sylibr 236	1 ⊢ (𝜒 → Ⅎ𝑥𝜑)

Syntax hints:   → wi 4   ↔ wb 208  Ⅎwnf 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806

This theorem depends on definitions:  df-bi 209  df-ex 1777  df-nf 1781

This theorem is referenced by:  nfand  1894  nf3and  1895  nfbid  1899  nfexd  2344  dvelimhw  2362  nfexd2  2464  dvelimf  2466  nfmod2  2638  nfmodv  2639  nfeud2  2672  nfeudw  2673  nfeqd  2988  nfeld  2989  nfabdw  3000  nfabd  3001  nfabd2OLD  3003  nfned  3120  nfneld  3131  nfraldw  3223  nfrald  3224  nfrexd  3307  nfrexdg  3308  nfreud  3372  nfrmod  3373  nfreuw  3374  nfsbc1d  3789  nfsbcdw  3792  nfsbcd  3795  nfbrd  5104  bj-dvelimdv  34170  bj-nfexd  34424  wl-sb8eut  34807