Theorem abid2 2866

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

Syntax hints:   = wceq 1534   ∈ wcel 2099  {cab 2704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805

This theorem is referenced by:  csbid  3902  csbconstg  3908  csbie  3925  abss  4053  ssab  4054  abssi  4063  notab  4300  dfrab3  4305  notrab  4307  eusn  4730  uniintsn  4985  iunidOLD  5058  axrep6g  5287  csbexg  5304  imai  6071  dffv4  6888  orduniss2  7830  dfixp  8909  euen1b  9043  pwfir  9192  modom2  9261  infmap2  10233  cshwsexaOLD  14799  ustfn  24093  ustn0  24112  lrrecse  27846  lrrecpred  27848  fpwrelmap  32499  eulerpartlemgvv  33932  ballotlem2  34044  dffv5  35456  ptrest  37027  cnambfre  37076  cnvepresex  37742  pmapglb  39180  polval2N  39316  rngunsnply  42519  iocinico  42563