Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > abid2 | GIF version |
Description: A simplification of class abstraction. Theorem 5.2 of [Quine] p. 35. (Contributed by NM, 26-Dec-1993.) |
Ref | Expression |
---|---|
abid2 | ⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biid 170 | . . 3 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴) | |
2 | 1 | abbi2i 2279 | . 2 ⊢ 𝐴 = {𝑥 ∣ 𝑥 ∈ 𝐴} |
3 | 2 | eqcomi 2168 | 1 ⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴 |
Colors of variables: wff set class |
Syntax hints: = wceq 1342 ∈ wcel 2135 {cab 2150 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-11 1493 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 |
This theorem is referenced by: csbid 3048 abss 3206 ssab 3207 abssi 3212 notab 3387 inrab2 3390 dfrab2 3392 dfrab3 3393 notrab 3394 eusn 3644 dfopg 3750 iunid 3915 csbexga 4104 imai 4954 dffv4g 5477 frec0g 6356 dfixp 6657 euen1b 6760 acfun 7154 ccfunen 7196 |
Copyright terms: Public domain | W3C validator |