Theorem abid2 2895

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

Syntax hints:   = wceq 1539   ∈ wcel 2112  {cab 2736

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 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1542  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831

This theorem is referenced by:  csbid  3819  abss  3966  ssab  3967  abssi  3975  notab  4208  dfrab3  4213  notrab  4215  eusn  4621  uniintsn  4875  iunid  4947  csbexg  5178  imai  5912  dffv4  6653  orduniss2  7545  dfixp  8479  euen1b  8597  modom2  8739  infmap2  9668  cshwsexa  14223  ustfn  22892  ustn0  22911  fpwrelmap  30582  eulerpartlemgvv  31852  ballotlem2  31964  lrrecse  33636  lrrecpred  33638  addsid1  33665  dffv5  33765  ptrest  35326  cnambfre  35375  cnvepresex  36021  pmapglb  37336  polval2N  37472  rngunsnply  40480  iocinico  40525