Theorem uneq2 4113

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

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

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 3438  df-un 3908

This theorem is referenced by:  uneq12  4114  uneq2i  4116  uneq2d  4119  uneqin  4240  disjssun  4419  unexbOLD  7684  undifixp  8861  unfi  9085  unxpdom  9148  ackbij1lem16  10128  fin23lem28  10234  ttukeylem6  10408  lcmfun  16556  ipodrsima  18447  mplsubglem  21906  mretopd  22977  iscldtop  22980  dfconn2  23304  nconnsubb  23308  comppfsc  23417  noextendseq  27577  onscutlt  28170  spanun  31489  constrextdg2lem  33715  locfinref  33808  isros  34135  unelros  34138  difelros  34139  rossros  34147  inelcarsg  34279  fineqvac  35072  rankung  36144  bj-funun  37230  paddval  39781  dochsatshp  41434  nacsfix  42689  eldioph4b  42788  eldioph4i  42789  fiuneneq  43169  isotone1  44025  fiiuncl  45047