Theorem unidm 4097

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 4096	1 ⊢ (𝐴 ∪ 𝐴) = 𝐴

Syntax hints:   = wceq 1540   ∈ wcel 2105   ∪ cun 3895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3443  df-un 3902

This theorem is referenced by:  unundi  4115  unundir  4116  uneqin  4223  difabs  4238  undifabs  4422  dfif5  4487  dfsn2  4584  unisng  4871  dfdm2  6206  unixpid  6209  fun2  6674  resasplit  6681  xpider  8625  pm54.43  9830  dmtrclfv  14801  lefld  18380  symg2bas  19069  gsumzaddlem  19590  pwssplit1  20393  plyun0  25430  wlkp1  28158  cycpmco2f1  31499  carsgsigalem  32388  sseqf  32465  probun  32492  nodenselem5  33949  filnetlem3  34627  pibt2  35644  metakunt21  40353  metakunt22  40354  metakunt24  40356  mapfzcons  40741  diophin  40797  pwssplit4  41118  fiuneneq  41226  rclexi  41444  rtrclex  41446  dfrtrcl5  41458  dfrcl2  41503  iunrelexp0  41531  relexpiidm  41533  corclrcl  41536  relexp01min  41542  cotrcltrcl  41554  clsk1indlem3  41874  fiiuncl  42834  fzopredsuc  45067