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 1859 | . 2 ⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓) |
4 | 1, 3 | sylibr 237 | 1 ⊢ (𝜒 → Ⅎ𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 Ⅎwnf 1791 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 |
This theorem depends on definitions: df-bi 210 df-ex 1788 df-nf 1792 |
This theorem is referenced by: nfand 1905 nf3and 1906 nfbid 1910 nfexd 2329 dvelimhw 2347 nfexd2 2446 dvelimf 2448 nfmod2 2558 nfmodv 2559 nfeud2 2590 nfeudw 2591 nfeqd 2915 nfeld 2916 nfabdw 2928 nfabdwOLD 2929 nfabd 2930 nfned 3044 nfneld 3055 nfraldw 3145 nfraldwOLD 3146 nfrald 3147 nfrexd 3234 nfrexdg 3235 nfreud 3296 nfrmod 3297 nfreuw 3298 nfsbc1d 3726 nfsbcdw 3729 nfsbcd 3732 nfbrd 5113 bj-dvelimdv 34798 bj-nfexd 35070 wl-sb8eut 35495 |
Copyright terms: Public domain | W3C validator |