Theorem abid2 2957

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

Syntax hints:   = wceq 1533   ∈ wcel 2110  {cab 2799

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1536  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893

This theorem is referenced by:  csbid  3895  abss  4039  ssab  4040  abssi  4045  notab  4272  dfrab3  4277  notrab  4279  eusn  4659  uniintsn  4905  iunid  4976  csbexg  5206  imai  5936  dffv4  6661  orduniss2  7542  dfixp  8457  euen1b  8574  modom2  8714  infmap2  9634  cshwsexa  14180  ustfn  22804  ustn0  22823  fpwrelmap  30463  eulerpartlemgvv  31629  ballotlem2  31741  dffv5  33380  ptrest  34885  cnambfre  34934  cnvepresex  35585  pmapglb  36900  polval2N  37036  rngunsnply  39766  iocinico  39811