Theorem nfxfrd 1855

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

Syntax hints:   → wi 4   ↔ wb 209  Ⅎwnf 1785

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

This theorem depends on definitions:  df-bi 210  df-ex 1782  df-nf 1786

This theorem is referenced by:  nfand  1898  nf3and  1899  nfbid  1903  nfexd  2337  dvelimhw  2355  nfexd2  2457  dvelimf  2459  nfmod2  2617  nfmodv  2618  nfeud2  2651  nfeudw  2652  nfeqd  2965  nfeld  2966  nfabdw  2976  nfabd  2977  nfned  3088  nfneld  3099  nfraldw  3187  nfrald  3188  nfrexd  3266  nfrexdg  3267  nfreud  3325  nfrmod  3326  nfreuw  3327  nfsbc1d  3738  nfsbcdw  3741  nfsbcd  3744  nfbrd  5076  bj-dvelimdv  34290  bj-nfexd  34553  wl-sb8eut  34978