New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > nfxfr | GIF version |
Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Ref | Expression |
---|---|
nfbii.1 | ⊢ (φ ↔ ψ) |
nfxfr.2 | ⊢ Ⅎxψ |
Ref | Expression |
---|---|
nfxfr | ⊢ Ⅎxφ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfxfr.2 | . 2 ⊢ Ⅎxψ | |
2 | nfbii.1 | . . 3 ⊢ (φ ↔ ψ) | |
3 | 2 | nfbii 1569 | . 2 ⊢ (Ⅎxφ ↔ Ⅎxψ) |
4 | 1, 3 | mpbir 200 | 1 ⊢ Ⅎxφ |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 176 Ⅎwnf 1544 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 |
This theorem depends on definitions: df-bi 177 df-nf 1545 |
This theorem is referenced by: nfnf1 1790 nfnan 1825 nfanOLD 1826 nf3an 1827 nfbiOLD 1835 nfor 1836 nf3or 1837 nfexOLD 1844 nfnf 1845 nfnfOLD 1846 nfs1f 2030 nfeu1 2214 nfmo1 2215 sb8eu 2222 nfnfc1 2492 nfnfc 2495 nfeq 2496 nfel 2497 nfne 2610 nfnel 2611 nfra1 2664 nfrex 2669 nfre1 2670 nfreu1 2781 nfrmo1 2782 nfrmo 2786 nfss 3266 sb8iota 4346 nffun 5130 nffn 5180 nff 5221 nff1 5256 nffo 5268 nff1o 5285 nfiso 5487 |
Copyright terms: Public domain | W3C validator |