![]() |
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 2881. See comments there. (Contributed by NM, 26-Dec-1993.) |
Ref | Expression |
---|---|
abid2 | ⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | abid1 2881 | . 2 ⊢ 𝐴 = {𝑥 ∣ 𝑥 ∈ 𝐴} | |
2 | 1 | eqcomi 2749 | 1 ⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1537 ∈ wcel 2108 {cab 2717 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2711 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1540 df-ex 1778 df-sb 2065 df-clab 2718 df-cleq 2732 df-clel 2819 |
This theorem is referenced by: csbid 3934 csbconstg 3940 csbie 3957 abss 4086 ssab 4087 abssi 4093 notab 4333 dfrab3 4338 notrab 4341 eusn 4755 uniintsn 5009 iunidOLD 5084 axrep6g 5311 csbexg 5328 imai 6105 dffv4 6919 orduniss2 7871 dfixp 8959 euen1b 9094 modom2 9310 pwfir 9385 infmap2 10288 cshwsexaOLD 14875 ustfn 24233 ustn0 24252 lrrecse 27995 lrrecpred 27997 fpwrelmap 32749 eulerpartlemgvv 34343 ballotlem2 34455 dffv5 35890 ptrest 37581 cnambfre 37630 cnvepresex 38292 pmapglb 39729 polval2N 39865 rngunsnply 43132 iocinico 43175 |
Copyright terms: Public domain | W3C validator |