![]() |
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 2227 | . 2 ⊢ 𝐴 = {𝑥 ∣ 𝑥 ∈ 𝐴} |
3 | 2 | eqcomi 2117 | 1 ⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴 |
Colors of variables: wff set class |
Syntax hints: = wceq 1312 ∈ wcel 1461 {cab 2099 |
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-5 1404 ax-7 1405 ax-gen 1406 ax-ie1 1450 ax-ie2 1451 ax-8 1463 ax-11 1465 ax-4 1468 ax-17 1487 ax-i9 1491 ax-ial 1495 ax-i5r 1496 ax-ext 2095 |
This theorem depends on definitions: df-bi 116 df-nf 1418 df-sb 1717 df-clab 2100 df-cleq 2106 df-clel 2109 |
This theorem is referenced by: csbid 2976 abss 3130 ssab 3131 abssi 3136 notab 3310 inrab2 3313 dfrab2 3315 dfrab3 3316 notrab 3317 eusn 3561 dfopg 3667 iunid 3832 csbexga 4014 imai 4851 dffv4g 5370 frec0g 6245 dfixp 6545 euen1b 6648 acfun 7007 |
Copyright terms: Public domain | W3C validator |