| 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 1852 | . 2 ⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓) |
| 4 | 1, 3 | sylibr 234 | 1 ⊢ (𝜒 → Ⅎ𝑥𝜑) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 Ⅎwnf 1783 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 |
| This theorem depends on definitions: df-bi 207 df-ex 1780 df-nf 1784 |
| This theorem is referenced by: nfand 1897 nf3and 1898 nfbid 1902 nfexd 2329 dvelimhw 2347 nfexd2 2451 dvelimf 2453 nfmod2 2558 nfmodv 2559 nfeud2 2590 nfeudw 2591 nfeqd 2916 nfeld 2917 nfabdw 2927 nfabd 2928 nfned 3044 nfneld 3055 nfraldw 3309 nfrexdw 3310 nfrald 3372 nfrexd 3373 nfreuwOLD 3426 nfrmod 3432 nfreud 3433 nfsbc1d 3806 nfsbcdw 3809 nfsbcd 3812 nfbrd 5189 bj-dvelimdv 36852 bj-nfexd 37139 wl-sb8eut 37579 wl-sb8eutv 37580 |
| Copyright terms: Public domain | W3C validator |