Theorem unidm 4086

Description: Idempotent law for union of classes. Theorem 23 of [Suppes] p. 27. (Contributed by NM, 21-Jun-1993.)

Assertion

Ref	Expression
unidm	⊢ (𝐴 ∪ 𝐴) = 𝐴

Proof of Theorem unidm

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		oridm 902	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐴) ↔ 𝑥 ∈ 𝐴)
2	1	uneqri 4085	1 ⊢ (𝐴 ∪ 𝐴) = 𝐴

Syntax hints:   = wceq 1539   ∈ wcel 2106   ∪ cun 3885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-un 3892

This theorem is referenced by:  unundi  4104  unundir  4105  uneqin  4212  difabs  4227  undifabs  4411  dfif5  4475  dfsn2  4574  unisng  4860  dfdm2  6184  unixpid  6187  fun2  6637  resasplit  6644  xpider  8577  pm54.43  9759  dmtrclfv  14729  lefld  18310  symg2bas  19000  gsumzaddlem  19522  pwssplit1  20321  plyun0  25358  wlkp1  28049  cycpmco2f1  31391  carsgsigalem  32282  sseqf  32359  probun  32386  nodenselem5  33891  filnetlem3  34569  pibt2  35588  metakunt21  40145  metakunt22  40146  metakunt24  40148  mapfzcons  40538  diophin  40594  pwssplit4  40914  fiuneneq  41022  rclexi  41223  rtrclex  41225  dfrtrcl5  41237  dfrcl2  41282  iunrelexp0  41310  relexpiidm  41312  corclrcl  41315  relexp01min  41321  cotrcltrcl  41333  clsk1indlem3  41653  fiiuncl  42613  fzopredsuc  44815