Theorem uneq1 4108

Description: Equality theorem for the union of two classes. (Contributed by NM, 15-Jul-1993.)

Assertion

Ref	Expression
uneq1	⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))

Proof of Theorem uneq1

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq2 2850	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	orbi1d 930	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)))
3		elun 4100	. . 3 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶))
4		elun 4100	. . 3 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶))
5	2, 3, 4	3bitr4g 317	. 2 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ 𝑥 ∈ (𝐵 ∪ 𝐶)))
6	5	eqrdv 2759	1 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))

This proof depends on syntax axioms:   → wi 4   ∨ wo 861   = wceq 1570   ∈ wcel 2145   ∪ cun 3897

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904

This theorem is used by:  uneq2  4109  uneq12  4110  uneq1i  4111  uneq1d  4114  unineq  4234  prprc1  4726  relresfldOLD  6278  oarec  8563  xpider  8802  ralxpmap  8917  undifixp  8955  findcard2  9173  unxpdom  9243  enp1ilem  9262  pwfilem  9302  domunfican  9306  rankung  9866  fin1a2lem10  10480  incexclem  15998  lcmfunsnlem  16809  ramub1lem1  17197  ramub1  17199  mreexexlem3d  17813  mreexexlem4d  17814  ipodrsima  18708  mplsubglem  22299  mretopd  23403  iscldtop  23406  nconnsubb  23734  plyval  26504  spanun  32140  difeq  33107  unelldsys  34784  isros  34794  unelros  34797  difelros  34798  rossros  34806  measun  34837  inelcarsg  34936  actfunsnf1o  35226  actfunsnrndisj  35227  mrsubvrs  36266  altopthsn  36706  bj-adjg1  37936  poimirlem28  38546  islshp  40016  lshpset2N  40156  paddval  40835  nacsfix  43702  eldioph4b  43797  eldioph4i  43798  diophren  43799  clsk3nimkb  45025  isotone1  45033  fiiuncl  46051  founiiun0  46174  infxrpnf  46425  meadjun  47441  hoidmvle  47579