Theorem abid2 2881

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817

This theorem is referenced by:  csbid  3841  csbconstg  3847  csbie  3864  abss  3990  ssab  3991  abssi  3999  notab  4235  dfrab3  4240  notrab  4242  eusn  4663  uniintsn  4915  iunid  4986  csbexg  5229  imai  5971  dffv4  6753  orduniss2  7655  dfixp  8645  euen1b  8771  pwfir  8921  modom2  8954  infmap2  9905  cshwsexa  14465  ustfn  23261  ustn0  23280  fpwrelmap  30970  eulerpartlemgvv  32243  ballotlem2  32355  lrrecse  34026  lrrecpred  34028  dffv5  34153  ptrest  35703  cnambfre  35752  cnvepresex  36396  pmapglb  37711  polval2N  37847  rngunsnply  40914  iocinico  40959