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  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  6071  dffv4  6886  orduniss2  7818  dfixp  8890  euen1b  9024  pwfir  9173  modom2  9242  infmap2  10210  cshwsexaOLD  14772  ustfn  23698  ustn0  23717  lrrecse  27416  lrrecpred  27418  fpwrelmap  31946  eulerpartlemgvv  33364  ballotlem2  33476  dffv5  34885  ptrest  36476  cnambfre  36525  cnvepresex  37192  pmapglb  38630  polval2N  38766  rngunsnply  41901  iocinico  41947