Theorem uneq2 4171

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

Syntax hints:   → wi 4   = wceq 1536   ∪ cun 3960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-un 3967

This theorem is referenced by:  uneq12  4172  uneq2i  4174  uneq2d  4177  uneqin  4294  disjssun  4473  unexbOLD  7766  undifixp  8972  unfi  9209  unxpdom  9286  ackbij1lem16  10271  fin23lem28  10377  ttukeylem6  10551  lcmfun  16678  ipodrsima  18598  mplsubglem  22036  mretopd  23115  iscldtop  23118  dfconn2  23442  nconnsubb  23446  comppfsc  23555  noextendseq  27726  spanun  31573  locfinref  33801  isros  34148  unelros  34151  difelros  34152  rossros  34160  inelcarsg  34292  fineqvac  35089  rankung  36147  bj-funun  37234  paddval  39780  dochsatshp  41433  nacsfix  42699  eldioph4b  42798  eldioph4i  42799  fiuneneq  43180  isotone1  44037  fiiuncl  45004