Theorem uneq2 4157

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

Syntax hints:   → wi 4   = wceq 1534   ∪ cun 3945

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3464  df-un 3952

This theorem is referenced by:  uneq12  4158  uneq2i  4160  uneq2d  4163  uneqin  4280  disjssun  4472  uniprgOLD  4934  unexb  7758  undifixp  8965  unfi  9212  unxpdom  9289  ackbij1lem16  10280  fin23lem28  10385  ttukeylem6  10559  lcmfun  16648  ipodrsima  18568  mplsubglem  22010  mretopd  23090  iscldtop  23093  dfconn2  23417  nconnsubb  23421  comppfsc  23530  noextendseq  27700  spanun  31481  locfinref  33658  isros  34003  unelros  34006  difelros  34007  rossros  34015  inelcarsg  34147  fineqvac  34935  rankung  35992  bj-funun  36961  paddval  39499  dochsatshp  41152  nacsfix  42387  eldioph4b  42486  eldioph4i  42487  fiuneneq  42875  isotone1  43733  fiiuncl  44684