![]() |
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 1948 | . 2 ⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓) |
4 | 1, 3 | sylibr 226 | 1 ⊢ (𝜒 → Ⅎ𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 Ⅎwnf 1879 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 |
This theorem depends on definitions: df-bi 199 df-ex 1876 df-nf 1880 |
This theorem is referenced by: nfand 1997 nf3and 1998 nfbid 2002 nfexd 2352 dvelimhw 2359 nfexd2 2453 dvelimf 2455 nfmod2 2603 nfmodv 2604 nfeud2 2630 nfeud2OLD 2641 nfmod2OLD 2642 nfeqd 2949 nfeld 2950 nfabd2 2961 nfned 3072 nfneld 3082 nfrald 3125 nfrexd 3186 nfreud 3293 nfrmod 3294 nfsbc1d 3651 nfsbcd 3654 nfbrd 4889 bj-dvelimdv 33328 wl-nfnbi 33804 wl-sb8eut 33849 |
Copyright terms: Public domain | W3C validator |