![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE 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 1359 | . 2 ⊢ (Ⅎxφ ↔ Ⅎxψ) |
4 | 1, 3 | mpbir 134 | 1 ⊢ Ⅎxφ |
Colors of variables: wff set class |
Syntax hints: ↔ wb 98 Ⅎwnf 1346 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1333 ax-gen 1335 |
This theorem depends on definitions: df-bi 110 df-nf 1347 |
This theorem is referenced by: nfnf1 1433 nf3an 1455 nfnf 1466 nfdc 1546 nfs1f 1660 nfeu1 1908 nfmo1 1909 sb8eu 1910 nfeu 1916 nfnfc1 2178 nfnfc 2181 nfeq 2182 nfel 2183 nfne 2291 nfnel 2298 nfra1 2349 nfre1 2359 nfreu1 2475 nfrmo1 2476 nfss 2932 rabn0m 3239 nfdisjv 3748 nfdisj1 3749 nfpo 4029 nfso 4030 nfse 4063 nfrel 4368 sb8iota 4817 nffun 4867 nffn 4938 nff 4986 nff1 5033 nffo 5048 nff1o 5067 nfiso 5389 |
Copyright terms: Public domain | W3C validator |