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 2027 | . 2 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ [𝑥 / 𝑥]𝜑) | |
2 | sbid 1657 | . 2 ⊢ ([𝑥 / 𝑥]𝜑 ↔ 𝜑) | |
3 | 1, 2 | bitri 173 | 1 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 98 ∈ wcel 1393 [wsb 1645 {cab 2026 |
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-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-4 1400 ax-17 1419 ax-i9 1423 |
This theorem depends on definitions: df-bi 110 df-sb 1646 df-clab 2027 |
This theorem is referenced by: abeq2 2146 abeq2i 2148 abeq1i 2149 abeq2d 2150 abid2f 2202 elabgt 2684 elabgf 2685 ralab2 2705 rexab2 2707 sbccsbg 2878 sbccsb2g 2879 ss2ab 3008 abn0r 3243 tpid3g 3483 eluniab 3592 elintab 3626 iunab 3703 iinab 3718 intexabim 3906 iinexgm 3908 opm 3971 finds2 4324 dmmrnm 4554 sniota 4894 eusvobj2 5498 eloprabga 5591 indpi 6440 elabgf0 9916 |
Copyright terms: Public domain | W3C validator |