Theorem uneq2 4157

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

Syntax hints:   → wi 4   = wceq 1542   ∪ cun 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3953

This theorem is referenced by:  uneq12  4158  uneq2i  4160  uneq2d  4163  uneqin  4278  disjssun  4467  uniprgOLD  4928  unexb  7732  undifixp  8925  unfi  9169  unxpdom  9250  ackbij1lem16  10227  fin23lem28  10332  ttukeylem6  10506  lcmfun  16579  ipodrsima  18491  mplsubglem  21550  mretopd  22588  iscldtop  22591  dfconn2  22915  nconnsubb  22919  comppfsc  23028  noextendseq  27160  spanun  30786  locfinref  32810  isros  33155  unelros  33158  difelros  33159  rossros  33167  inelcarsg  33299  fineqvac  34086  rankung  35127  bj-funun  36122  paddval  38658  dochsatshp  40311  nacsfix  41436  eldioph4b  41535  eldioph4i  41536  fiuneneq  41925  isotone1  42785  fiiuncl  43738