Theorem abid2 2926

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

Syntax hints:   = wceq 1522   ∈ wcel 2081  {cab 2775

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1525  df-ex 1762  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863

This theorem is referenced by:  csbid  3823  abss  3961  ssab  3962  abssi  3967  notab  4193  dfrab3  4198  notrab  4200  eusn  4573  uniintsn  4819  iunid  4883  csbexg  5105  imai  5818  dffv4  6535  orduniss2  7404  dfixp  8312  euen1b  8428  modom2  8566  infmap2  9486  cshwsexa  14022  ustfn  22493  ustn0  22512  fpwrelmap  30157  eulerpartlemgvv  31251  ballotlem2  31363  dffv5  32994  ptrest  34422  cnambfre  34471  cnvepresex  35123  pmapglb  36437  polval2N  36573  rngunsnply  39258  iocinico  39303