Theorem abid2 2774

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

Syntax hints:   = wceq 1523   ∈ wcel 2030  {cab 2637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647

This theorem is referenced by:  csbid  3574  abss  3704  ssab  3705  abssi  3710  notab  3930  dfrab3  3935  notrab  3937  eusn  4297  uniintsn  4546  iunid  4607  csbexg  4825  imai  5513  dffv4  6226  orduniss2  7075  dfixp  7952  euen1b  8068  modom2  8203  infmap2  9078  cshwsexa  13616  ustfn  22052  ustn0  22071  fpwrelmap  29636  eulerpartlemgvv  30566  ballotlem2  30678  dffv5  32156  ptrest  33538  cnambfre  33588  cnvepresex  34245  pmapglb  35374  polval2N  35510  rngunsnply  38060  iocinico  38114