![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > abid | GIF version |
Description: Simplification of class abstraction notation when the free and bound variables are identical. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
abid | ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-clab 2087 | . 2 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ [𝑥 / 𝑥]𝜑) | |
2 | sbid 1715 | . 2 ⊢ ([𝑥 / 𝑥]𝜑 ↔ 𝜑) | |
3 | 1, 2 | bitri 183 | 1 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 ∈ wcel 1448 [wsb 1703 {cab 2086 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-8 1450 ax-4 1455 ax-17 1474 ax-i9 1478 |
This theorem depends on definitions: df-bi 116 df-sb 1704 df-clab 2087 |
This theorem is referenced by: abeq2 2208 abeq2i 2210 abeq1i 2211 abeq2d 2212 abid2f 2265 elabgt 2779 elabgf 2780 ralab2 2801 rexab2 2803 sbccsbg 2981 sbccsb2g 2982 ss2ab 3112 abn0r 3334 abn0m 3335 tpid3g 3585 eluniab 3695 elintab 3729 iunab 3806 iinab 3821 intexabim 4017 iinexgm 4019 opm 4094 finds2 4453 dmmrnm 4696 sniota 5051 eusvobj2 5692 eloprabga 5790 indpi 7051 elabgf0 12565 |
Copyright terms: Public domain | W3C validator |