Theorem uneq2 4115

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

Syntax hints:   → wi 4   = wceq 1560   ∪ cun 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-un 3909

This theorem is referenced by:  uneq12  4116  uneq2i  4118  uneq2d  4121  uneqin  4241  disjssun  4422  unexbOLD  7731  undifixp  8916  unfi  9139  unxpdom  9203  ackbij1lem16  10190  fin23lem28  10297  ttukeylem6  10471  lcmfun  16679  ipodrsima  18573  mplsubglem  22050  mretopd  23152  iscldtop  23155  dfconn2  23479  nconnsubb  23483  comppfsc  23592  noextendseq  27731  oncutlt  28357  spanun  31748  constrextdg2lem  34045  locfinref  34138  isros  34465  unelros  34468  difelros  34469  rossros  34477  inelcarsg  34608  fineqvac  35412  rankung  36516  bj-funun  37744  paddval  40422  dochsatshp  42075  nacsfix  43293  eldioph4b  43388  eldioph4i  43389  fiuneneq  43769  isotone1  44624  fiiuncl  45645