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  1932  nf3and  1933  nfbid  1937  nfexd  2363  dvelimhw  2378  nfexd2  2478  dvelimf  2480  nfmod2  2586  nfmodv  2587  nfeud2  2618  nfeudw  2619  nfeqd  2936  nfeld  2937  nfabdw  2947  nfabd  2948  nfned  3063  nfneld  3074  nfraldw  3311  nfrexdw  3312  nfrald  3361  nfrexd  3362  nfrmod  3412  nfreud  3413  nfsbc1d  3760  nfsbcdw  3763  nfsbcd  3766  nfbrd  5155  nfchnd  18817  bj-dvelimdv  37954  bj-nfexd  38262  wl-sb8eut  38715  wl-sb8eutv  38716