![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > abid2 | Structured version Visualization version GIF version |
Description: A simplification of class abstraction. Commuted form of abid1 2925. See comments there. (Contributed by NM, 26-Dec-1993.) |
Ref | Expression |
---|---|
abid2 | ⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | abid1 2925 | . 2 ⊢ 𝐴 = {𝑥 ∣ 𝑥 ∈ 𝐴} | |
2 | 1 | eqcomi 2804 | 1 ⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1522 ∈ wcel 2081 {cab 2775 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-ext 2769 |
This theorem depends on definitions: df-bi 208 df-an 397 df-tru 1525 df-ex 1762 df-sb 2043 df-clab 2776 df-cleq 2788 df-clel 2863 |
This theorem is referenced by: csbid 3823 abss 3961 ssab 3962 abssi 3967 notab 4193 dfrab3 4198 notrab 4200 eusn 4573 uniintsn 4819 iunid 4883 csbexg 5105 imai 5818 dffv4 6535 orduniss2 7404 dfixp 8312 euen1b 8428 modom2 8566 infmap2 9486 cshwsexa 14022 ustfn 22493 ustn0 22512 fpwrelmap 30157 eulerpartlemgvv 31251 ballotlem2 31363 dffv5 32994 ptrest 34422 cnambfre 34471 cnvepresex 35123 pmapglb 36437 polval2N 36573 rngunsnply 39258 iocinico 39303 |
Copyright terms: Public domain | W3C validator |