Theorem abid2 2863

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

Syntax hints:   = wceq 1533   ∈ wcel 2098  {cab 2702

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802

This theorem is referenced by:  csbid  3898  csbconstg  3904  csbie  3921  abss  4050  ssab  4051  abssi  4059  notab  4299  dfrab3  4304  notrab  4307  eusn  4730  uniintsn  4985  iunidOLD  5059  axrep6g  5288  csbexg  5305  imai  6072  dffv4  6888  orduniss2  7833  dfixp  8914  euen1b  9048  pwfir  9197  modom2  9266  infmap2  10239  cshwsexaOLD  14805  ustfn  24122  ustn0  24141  lrrecse  27875  lrrecpred  27877  fpwrelmap  32558  eulerpartlemgvv  34052  ballotlem2  34164  dffv5  35576  ptrest  37148  cnambfre  37197  cnvepresex  37861  pmapglb  39298  polval2N  39434  rngunsnply  42661  iocinico  42704

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »