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 2959. See comments there. (Contributed by NM, 26-Dec-1993.) |
Ref | Expression |
---|---|
abid2 | ⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | abid1 2959 | . 2 ⊢ 𝐴 = {𝑥 ∣ 𝑥 ∈ 𝐴} | |
2 | 1 | eqcomi 2833 | 1 ⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1536 ∈ wcel 2113 {cab 2802 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-ext 2796 |
This theorem depends on definitions: df-bi 209 df-an 399 df-tru 1539 df-ex 1780 df-sb 2069 df-clab 2803 df-cleq 2817 df-clel 2896 |
This theorem is referenced by: csbid 3899 abss 4043 ssab 4044 abssi 4049 notab 4276 dfrab3 4281 notrab 4283 eusn 4669 uniintsn 4916 iunid 4987 csbexg 5217 imai 5945 dffv4 6670 orduniss2 7551 dfixp 8466 euen1b 8583 modom2 8723 infmap2 9643 cshwsexa 14189 ustfn 22813 ustn0 22832 fpwrelmap 30472 eulerpartlemgvv 31638 ballotlem2 31750 dffv5 33389 ptrest 34895 cnambfre 34944 cnvepresex 35595 pmapglb 36910 polval2N 37046 rngunsnply 39779 iocinico 39824 |
Copyright terms: Public domain | W3C validator |