Theorem uneq2 4112

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

Syntax hints:   → wi 4   = wceq 1541   ∪ cun 3897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-un 3904

This theorem is referenced by:  uneq12  4113  uneq2i  4115  uneq2d  4118  uneqin  4239  disjssun  4418  unexbOLD  7691  undifixp  8870  unfi  9093  unxpdom  9157  ackbij1lem16  10142  fin23lem28  10248  ttukeylem6  10422  lcmfun  16570  ipodrsima  18462  mplsubglem  21952  mretopd  23034  iscldtop  23037  dfconn2  23361  nconnsubb  23365  comppfsc  23474  noextendseq  27633  onscutlt  28232  spanun  31569  constrextdg2lem  33854  locfinref  33947  isros  34274  unelros  34277  difelros  34278  rossros  34286  inelcarsg  34417  fineqvac  35221  rankung  36309  bj-funun  37396  paddval  39997  dochsatshp  41650  nacsfix  42896  eldioph4b  42995  eldioph4i  42996  fiuneneq  43376  isotone1  44231  fiiuncl  45252