Theorem uneq2 4114

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

Syntax hints:   → wi 4   = wceq 1541   ∪ cun 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906

This theorem is referenced by:  uneq12  4115  uneq2i  4117  uneq2d  4120  uneqin  4241  disjssun  4420  unexbOLD  7693  undifixp  8872  unfi  9095  unxpdom  9159  ackbij1lem16  10144  fin23lem28  10250  ttukeylem6  10424  lcmfun  16572  ipodrsima  18464  mplsubglem  21954  mretopd  23036  iscldtop  23039  dfconn2  23363  nconnsubb  23367  comppfsc  23476  noextendseq  27635  oncutlt  28260  spanun  31620  constrextdg2lem  33905  locfinref  33998  isros  34325  unelros  34328  difelros  34329  rossros  34337  inelcarsg  34468  fineqvac  35272  rankung  36360  bj-funun  37457  paddval  40058  dochsatshp  41711  nacsfix  42954  eldioph4b  43053  eldioph4i  43054  fiuneneq  43434  isotone1  44289  fiiuncl  45310