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  2361  dvelimhw  2376  nfexd2  2477  dvelimf  2479  nfmod2  2585  nfmodv  2586  nfeud2  2617  nfeudw  2618  nfeqd  2934  nfeld  2935  nfabdw  2945  nfabd  2946  nfned  3061  nfneld  3072  nfraldw  3309  nfrexdw  3310  nfrald  3359  nfrexd  3360  nfrmod  3410  nfreud  3411  nfsbc1d  3760  nfsbcdw  3763  nfsbcd  3766  nfbrd  5155  nfchnd  18705  bj-dvelimdv  37602  bj-nfexd  37896  wl-sb8eut  38349  wl-sb8eutv  38350