Theorem uneq2 4092

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

Syntax hints:   → wi 4   = wceq 1547   ∪ cun 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888

This theorem is referenced by:  uneq12  4093  uneq2i  4095  uneq2d  4098  uneqin  4217  disjssun  4396  unexbOLD  7691  undifixp  8872  unfi  9095  unxpdom  9159  ackbij1lem16  10147  fin23lem28  10253  ttukeylem6  10427  lcmfun  16605  ipodrsima  18498  mplsubglem  21973  mretopd  23075  iscldtop  23078  dfconn2  23402  nconnsubb  23406  comppfsc  23515  noextendseq  27649  oncutlt  28274  spanun  31634  constrextdg2lem  33932  locfinref  34025  isros  34352  unelros  34355  difelros  34356  rossros  34364  inelcarsg  34495  fineqvac  35297  rankung  36394  bj-funun  37612  paddval  40290  dochsatshp  41943  nacsfix  43161  eldioph4b  43256  eldioph4i  43257  fiuneneq  43637  isotone1  44492  fiiuncl  45513