Theorem nfxfrd 1887

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ex 1813  df-nf 1817

This theorem is used by:  nfand  1930  nf3and  1931  nfbid  1935  nfexd  2365  dvelimhw  2380  nfexd2  2481  dvelimf  2483  nfmod2  2589  nfmodv  2590  nfeud2  2621  nfeudw  2622  nfeqd  2938  nfeld  2939  nfabdw  2949  nfabd  2950  nfned  3065  nfneld  3076  nfraldw  3313  nfrexdw  3314  nfrald  3364  nfrexd  3365  nfrmod  3415  nfreud  3416  nfsbc1d  3765  nfsbcdw  3768  nfsbcd  3771  nfbrd  5162  nfchnd  18692  bj-dvelimdv  37527  bj-nfexd  37821  wl-sb8eut  38274  wl-sb8eutv  38275