Theorem uneq2 3989

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

Syntax hints:   → wi 4   = wceq 1658   ∪ cun 3797

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2804

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-v 3417  df-un 3804

This theorem is referenced by:  uneq12  3990  uneq2i  3992  uneq2d  3995  uneqin  4109  disjssun  4260  uniprg  4673  unexb  7219  undifixp  8212  unxpdom  8437  ackbij1lem16  9373  fin23lem28  9478  ttukeylem6  9652  lcmfun  15732  ipodrsima  17519  mplsubglem  19796  mretopd  21268  iscldtop  21271  dfconn2  21594  nconnsubb  21598  comppfsc  21707  spanun  28960  locfinref  30454  isros  30777  unelros  30780  difelros  30781  rossros  30789  inelcarsg  30919  noextendseq  32360  rankung  32813  bj-funun  33680  paddval  35874  dochsatshp  37527  nacsfix  38120  eldioph4b  38220  eldioph4i  38221  fiuneneq  38619  isotone1  39187  fiiuncl  40052