Theorem nfxfrd 1886

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

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

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

This proof depends on definitions:  df-bi 210  df-ex 1812  df-nf 1816

This theorem is used by:  nfand  1929  nf3and  1930  nfbid  1934  nfexd  2359  dvelimhw  2374  nfexd2  2475  dvelimf  2477  nfmod2  2583  nfmodv  2584  nfeud2  2615  nfeudw  2616  nfeqd  2932  nfeld  2933  nfabdw  2943  nfabd  2944  nfned  3059  nfneld  3070  nfraldw  3307  nfrexdw  3308  nfrald  3357  nfrexd  3358  nfrmod  3408  nfreud  3409  nfsbc1d  3756  nfsbcdw  3759  nfsbcd  3762  nfbrd  5150  nfchnd  18790  bj-dvelimdv  37855  bj-nfexd  38150  wl-sb8eut  38603  wl-sb8eutv  38604