Theorem uneq2 4125

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

Assertion

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

Proof of Theorem uneq2

Step	Hyp	Ref	Expression
1		uneq1 4124	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))
2		uncom 4121	. 2 ⊢ (𝐶 ∪ 𝐴) = (𝐴 ∪ 𝐶)
3		uncom 4121	. 2 ⊢ (𝐶 ∪ 𝐵) = (𝐵 ∪ 𝐶)
4	1, 2, 3	3eqtr4g 2789	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵))

Syntax hints:   → wi 4   = wceq 1540   ∪ cun 3912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919

This theorem is referenced by:  uneq12  4126  uneq2i  4128  uneq2d  4131  uneqin  4252  disjssun  4431  unexbOLD  7724  undifixp  8907  unfi  9135  unxpdom  9200  ackbij1lem16  10187  fin23lem28  10293  ttukeylem6  10467  lcmfun  16615  ipodrsima  18500  mplsubglem  21908  mretopd  22979  iscldtop  22982  dfconn2  23306  nconnsubb  23310  comppfsc  23419  noextendseq  27579  onscutlt  28165  spanun  31474  constrextdg2lem  33738  locfinref  33831  isros  34158  unelros  34161  difelros  34162  rossros  34170  inelcarsg  34302  fineqvac  35087  rankung  36154  bj-funun  37240  paddval  39792  dochsatshp  41445  nacsfix  42700  eldioph4b  42799  eldioph4i  42800  fiuneneq  43181  isotone1  44037  fiiuncl  45059