Theorem abid2 2879

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

Syntax hints:   = wceq 1539   ∈ wcel 2108  {cab 2714

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816

This theorem is referenced by:  csbid  3924  csbconstg  3930  csbie  3947  abss  4076  ssab  4077  abssi  4083  notab  4323  dfrab3  4328  notrab  4331  eusn  4738  uniintsn  4993  iunidOLD  5069  axrep6g  5299  csbexg  5319  imai  6099  dffv4  6911  orduniss2  7860  dfixp  8947  euen1b  9076  modom2  9288  pwfir  9362  infmap2  10264  cshwsexaOLD  14869  ustfn  24235  ustn0  24254  lrrecse  28001  lrrecpred  28003  fpwrelmap  32765  eulerpartlemgvv  34372  ballotlem2  34484  dffv5  35919  ptrest  37620  cnambfre  37669  cnvepresex  38330  pmapglb  39767  polval2N  39903  rngunsnply  43174  iocinico  43217