![]() |
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 2773. See comments there. (Contributed by NM, 26-Dec-1993.) |
Ref | Expression |
---|---|
abid2 | ⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | abid1 2773 | . 2 ⊢ 𝐴 = {𝑥 ∣ 𝑥 ∈ 𝐴} | |
2 | 1 | eqcomi 2660 | 1 ⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1523 ∈ wcel 2030 {cab 2637 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 |
This theorem is referenced by: csbid 3574 abss 3704 ssab 3705 abssi 3710 notab 3930 dfrab3 3935 notrab 3937 eusn 4297 uniintsn 4546 iunid 4607 csbexg 4825 imai 5513 dffv4 6226 orduniss2 7075 dfixp 7952 euen1b 8068 modom2 8203 infmap2 9078 cshwsexa 13616 ustfn 22052 ustn0 22071 fpwrelmap 29636 eulerpartlemgvv 30566 ballotlem2 30678 dffv5 32156 ptrest 33538 cnambfre 33588 cnvepresex 34245 pmapglb 35374 polval2N 35510 rngunsnply 38060 iocinico 38114 |
Copyright terms: Public domain | W3C validator |