Theorem abid2 2872

Description: A simplification of class abstraction. Commuted form of abid1 2871. 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 2871	. 2 ⊢ 𝐴 = {𝑥 ∣ 𝑥 ∈ 𝐴}
2	1	eqcomi 2742	1 ⊢ {𝑥 ∣ 𝑥 ∈ 𝐴} = 𝐴

Syntax hints:   = wceq 1542   ∈ wcel 2107  {cab 2710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811

This theorem is referenced by:  csbid  3907  csbconstg  3913  csbie  3930  abss  4058  ssab  4059  abssi  4068  notab  4305  dfrab3  4310  notrab  4312  eusn  4735  uniintsn  4992  iunidOLD  5065  axrep6g  5294  csbexg  5311  imai  6074  dffv4  6889  orduniss2  7821  dfixp  8893  euen1b  9027  pwfir  9176  modom2  9245  infmap2  10213  cshwsexaOLD  14775  ustfn  23706  ustn0  23725  lrrecse  27426  lrrecpred  27428  fpwrelmap  31958  eulerpartlemgvv  33375  ballotlem2  33487  dffv5  34896  ptrest  36487  cnambfre  36536  cnvepresex  37203  pmapglb  38641  polval2N  38777  rngunsnply  41915  iocinico  41961