Theorem uneq2 4124

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

Syntax hints:   → wi 4   = wceq 1567   ∪ cun 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918

This theorem is referenced by:  uneq12  4125  uneq2i  4127  uneq2d  4130  uneqin  4250  disjssun  4434  unexbOLD  7747  undifixp  8932  unfi  9155  unxpdom  9219  ackbij1lem16  10217  fin23lem28  10324  ttukeylem6  10498  lcmfun  16703  ipodrsima  18597  mplsubglem  22117  mretopd  23218  iscldtop  23221  dfconn2  23545  nconnsubb  23549  comppfsc  23658  noextendseq  27797  oncutlt  28423  spanun  31838  constrextdg2lem  34083  locfinref  34176  isros  34503  unelros  34506  difelros  34507  rossros  34515  inelcarsg  34646  fineqvac  35452  rankung  36557  bj-funun  37784  paddval  40462  dochsatshp  42115  nacsfix  43335  eldioph4b  43430  eldioph4i  43431  fiuneneq  43811  isotone1  44666  fiiuncl  45677