Theorem nfxfrd 1881

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

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

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

This theorem depends on definitions:  df-bi 210  df-ex 1807  df-nf 1811

This theorem is referenced by:  nfand  1924  nf3and  1925  nfbid  1929  nfexd  2368  dvelimhw  2383  nfexd2  2484  dvelimf  2486  nfmod2  2592  nfmodv  2593  nfeud2  2624  nfeudw  2625  nfeqd  2941  nfeld  2942  nfabdw  2952  nfabd  2953  nfned  3068  nfneld  3079  nfraldw  3316  nfrexdw  3317  nfrald  3368  nfrexd  3369  nfrmod  3419  nfreud  3420  nfsbc1d  3771  nfsbcdw  3774  nfsbcd  3777  nfbrd  5161  nfchnd  18669  bj-dvelimdv  37411  bj-nfexd  37705  wl-sb8eut  38158  wl-sb8eutv  38159