Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nfxfrd | Structured version Visualization version GIF version |
Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Ref | Expression |
---|---|
nfbii.1 | ⊢ (𝜑 ↔ 𝜓) |
nfxfrd.2 | ⊢ (𝜒 → Ⅎ𝑥𝜓) |
Ref | Expression |
---|---|
nfxfrd | ⊢ (𝜒 → Ⅎ𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfxfrd.2 | . 2 ⊢ (𝜒 → Ⅎ𝑥𝜓) | |
2 | nfbii.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
3 | 2 | nfbii 1778 | . 2 ⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓) |
4 | 1, 3 | sylibr 224 | 1 ⊢ (𝜒 → Ⅎ𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 Ⅎwnf 1708 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 |
This theorem depends on definitions: df-bi 197 df-ex 1705 df-nf 1710 |
This theorem is referenced by: nfand 1826 nf3and 1827 nfbid 1832 nfexd 2167 dvelimhw 2173 nfexd2 2332 dvelimf 2334 nfeud2 2482 nfmod2 2483 nfeqd 2772 nfeld 2773 nfabd2 2784 nfned 2895 nfneld 2905 nfrald 2944 nfrexd 3006 nfreud 3112 nfrmod 3113 nfsbc1d 3453 nfsbcd 3456 nfbrd 4698 bj-dvelimdv 32834 wl-nfnbi 33314 wl-sb8eut 33359 |
Copyright terms: Public domain | W3C validator |