![]() |
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 | ⊢ Ⅎ𝑥𝜓 |
Ref | Expression |
---|---|
nfxfr | ⊢ Ⅎ𝑥𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfxfr.2 | . 2 ⊢ Ⅎ𝑥𝜓 | |
2 | nfbii.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
3 | 2 | nfbii 1473 | . 2 ⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓) |
4 | 1, 3 | mpbir 146 | 1 ⊢ Ⅎ𝑥𝜑 |
Colors of variables: wff set class |
Syntax hints: ↔ wb 105 Ⅎwnf 1460 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 |
This theorem depends on definitions: df-bi 117 df-nf 1461 |
This theorem is referenced by: nfnf1 1544 nf3an 1566 nfnf 1577 nfdc 1659 nfs1f 1780 nfsbv 1947 nfeu1 2037 nfmo1 2038 sb8eu 2039 nfeu 2045 nfnfc1 2322 nfnfc 2326 nfeq 2327 nfel 2328 nfabdw 2338 nfne 2440 nfnel 2449 nfra1 2508 nfre1 2520 nfreu1 2648 nfrmo1 2649 nfss 3148 rabn0m 3450 nfdisjv 3992 nfdisj1 3993 nfpo 4301 nfso 4302 nfse 4341 nffrfor 4348 nffr 4349 nfwe 4355 nfrel 4711 sb8iota 5185 nffun 5239 nffn 5312 nff 5362 nff1 5419 nffo 5437 nff1o 5459 nfiso 5806 nfixpxy 6716 |
Copyright terms: Public domain | W3C validator |