Theorem abid2 2876

Description: A simplification of class abstraction. Commuted form of abid1 2875. See comments there. (Contributed by NM, 26-Dec-1993.)

Assertion

Ref	Expression
abid2	⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴

Distinct variable group:   𝑥,𝐴

Proof of Theorem abid2

Step	Hyp	Ref	Expression
1		abid1 2875	. 2 ⊢ 𝐴 = {𝑥 ∣ 𝑥 ∈ 𝐴}
2	1	eqcomi 2743	1 ⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴

Syntax hints:   = wceq 1537   ∈ wcel 2103  {cab 2711

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 2105  ax-9 2113  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2712  df-cleq 2726  df-clel 2813

This theorem is referenced by:  csbid  3928  csbconstg  3934  csbie  3951  abss  4080  ssab  4081  abssi  4087  notab  4328  dfrab3  4333  notrab  4336  eusn  4755  uniintsn  5013  iunidOLD  5087  axrep6g  5314  csbexg  5331  imai  6102  dffv4  6916  orduniss2  7865  dfixp  8953  euen1b  9088  modom2  9304  pwfir  9379  infmap2  10282  cshwsexaOLD  14869  ustfn  24224  ustn0  24243  lrrecse  27984  lrrecpred  27986  fpwrelmap  32739  eulerpartlemgvv  34333  ballotlem2  34445  dffv5  35880  ptrest  37527  cnambfre  37576  cnvepresex  38238  pmapglb  39675  polval2N  39811  rngunsnply  43070  iocinico  43113