Theorem uneq2 4084

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

Syntax hints:   → wi 4   = wceq 1538   ∪ cun 3879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886

This theorem is referenced by:  uneq12  4085  uneq2i  4087  uneq2d  4090  uneqin  4205  disjssun  4375  uniprg  4818  unexb  7451  undifixp  8481  unxpdom  8709  ackbij1lem16  9646  fin23lem28  9751  ttukeylem6  9925  lcmfun  15979  ipodrsima  17767  mplsubglem  20672  mretopd  21697  iscldtop  21700  dfconn2  22024  nconnsubb  22028  comppfsc  22137  spanun  29328  locfinref  31194  isros  31537  unelros  31540  difelros  31541  rossros  31549  inelcarsg  31679  noextendseq  33287  rankung  33740  bj-funun  34667  paddval  37094  dochsatshp  38747  nacsfix  39653  eldioph4b  39752  eldioph4i  39753  fiuneneq  40141  isotone1  40751  fiiuncl  41699