Theorem uneq2 4128

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 4127	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))
2		uncom 4124	. 2 ⊢ (𝐶 ∪ 𝐴) = (𝐴 ∪ 𝐶)
3		uncom 4124	. 2 ⊢ (𝐶 ∪ 𝐵) = (𝐵 ∪ 𝐶)
4	1, 2, 3	3eqtr4g 2790	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵))

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

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922

This theorem is referenced by:  uneq12  4129  uneq2i  4131  uneq2d  4134  uneqin  4255  disjssun  4434  unexbOLD  7727  undifixp  8910  unfi  9141  unxpdom  9207  ackbij1lem16  10194  fin23lem28  10300  ttukeylem6  10474  lcmfun  16622  ipodrsima  18507  mplsubglem  21915  mretopd  22986  iscldtop  22989  dfconn2  23313  nconnsubb  23317  comppfsc  23426  noextendseq  27586  onscutlt  28172  spanun  31481  constrextdg2lem  33745  locfinref  33838  isros  34165  unelros  34168  difelros  34169  rossros  34177  inelcarsg  34309  fineqvac  35094  rankung  36161  bj-funun  37247  paddval  39799  dochsatshp  41452  nacsfix  42707  eldioph4b  42806  eldioph4i  42807  fiuneneq  43188  isotone1  44044  fiiuncl  45066