Theorem uneq2 3609

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

Syntax hints:   → wi 4   = wceq 1468   ∪ cun 3424

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485

This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-v 3068  df-un 3431

This theorem is referenced by:  uneq12  3610  uneq2i  3612  uneq2d  3615  uneqin  3721  disjssun  3862  uniprg  4242  sucprc  5549  unexb  6668  undifixp  7641  unxpdom  7863  ackbij1lem16  8750  fin23lem28  8855  ttukeylem6  9029  lcmfun  14780  ipodrsima  16576  mplsubglem  18817  mretopd  20265  iscldtop  20268  dfcon2  20591  nconsubb  20595  comppfsc  20704  spanun  27361  locfinref  28823  isros  29145  unelros  29148  difelros  29149  rossros  29157  inelcarsg  29297  nofulllem1  30742  rankung  31084  paddval  33603  dochsatshp  35259  nacsfix  35794  eldioph4b  35894  eldioph4i  35895  fiuneneq  36311  isotone1  36872  fiiuncl  37748