Theorem uneq2 4162

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956

This theorem is referenced by:  uneq12  4163  uneq2i  4165  uneq2d  4168  uneqin  4289  disjssun  4468  unexbOLD  7768  undifixp  8974  unfi  9211  unxpdom  9289  ackbij1lem16  10274  fin23lem28  10380  ttukeylem6  10554  lcmfun  16682  ipodrsima  18586  mplsubglem  22019  mretopd  23100  iscldtop  23103  dfconn2  23427  nconnsubb  23431  comppfsc  23540  noextendseq  27712  spanun  31564  constrextdg2lem  33789  locfinref  33840  isros  34169  unelros  34172  difelros  34173  rossros  34181  inelcarsg  34313  fineqvac  35111  rankung  36167  bj-funun  37253  paddval  39800  dochsatshp  41453  nacsfix  42723  eldioph4b  42822  eldioph4i  42823  fiuneneq  43204  isotone1  44061  fiiuncl  45070