Theorem uneq2 4121

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

Syntax hints:   → wi 4   = wceq 1540   ∪ cun 3909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-un 3916

This theorem is referenced by:  uneq12  4122  uneq2i  4124  uneq2d  4127  uneqin  4248  disjssun  4427  unexbOLD  7704  undifixp  8884  unfi  9112  unxpdom  9176  ackbij1lem16  10163  fin23lem28  10269  ttukeylem6  10443  lcmfun  16591  ipodrsima  18482  mplsubglem  21941  mretopd  23012  iscldtop  23015  dfconn2  23339  nconnsubb  23343  comppfsc  23452  noextendseq  27612  onscutlt  28205  spanun  31524  constrextdg2lem  33731  locfinref  33824  isros  34151  unelros  34154  difelros  34155  rossros  34163  inelcarsg  34295  fineqvac  35080  rankung  36147  bj-funun  37233  paddval  39785  dochsatshp  41438  nacsfix  42693  eldioph4b  42792  eldioph4i  42793  fiuneneq  43174  isotone1  44030  fiiuncl  45052