![]() |
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 2869. See comments there. (Contributed by NM, 26-Dec-1993.) |
Ref | Expression |
---|---|
abid2 | ⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | abid1 2869 | . 2 ⊢ 𝐴 = {𝑥 ∣ 𝑥 ∈ 𝐴} | |
2 | 1 | eqcomi 2740 | 1 ⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1540 ∈ wcel 2105 {cab 2708 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1543 df-ex 1781 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 |
This theorem is referenced by: csbid 3906 csbconstg 3912 csbie 3929 abss 4057 ssab 4058 abssi 4067 notab 4304 dfrab3 4309 notrab 4311 eusn 4734 uniintsn 4991 iunidOLD 5064 axrep6g 5293 csbexg 5310 imai 6073 dffv4 6888 orduniss2 7825 dfixp 8897 euen1b 9031 pwfir 9180 modom2 9249 infmap2 10217 cshwsexaOLD 14780 ustfn 23927 ustn0 23946 lrrecse 27665 lrrecpred 27667 fpwrelmap 32226 eulerpartlemgvv 33674 ballotlem2 33786 dffv5 35201 ptrest 36791 cnambfre 36840 cnvepresex 37507 pmapglb 38945 polval2N 39081 rngunsnply 42218 iocinico 42264 |
Copyright terms: Public domain | W3C validator |