Theorem nfxfrd 1950

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

Syntax hints:   → wi 4   ↔ wb 198  Ⅎwnf 1879

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

This theorem depends on definitions:  df-bi 199  df-ex 1876  df-nf 1880

This theorem is referenced by:  nfand  1997  nf3and  1998  nfbid  2002  nfexd  2352  dvelimhw  2359  nfexd2  2453  dvelimf  2455  nfmod2  2603  nfmodv  2604  nfeud2  2630  nfeud2OLD  2641  nfmod2OLD  2642  nfeqd  2949  nfeld  2950  nfabd2  2961  nfned  3072  nfneld  3082  nfrald  3125  nfrexd  3186  nfreud  3293  nfrmod  3294  nfsbc1d  3651  nfsbcd  3654  nfbrd  4889  bj-dvelimdv  33328  wl-nfnbi  33804  wl-sb8eut  33849