Theorem uneq2 4103

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

Syntax hints:   → wi 4   = wceq 1542   ∪ cun 3888

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895

This theorem is referenced by:  uneq12  4104  uneq2i  4106  uneq2d  4109  uneqin  4230  disjssun  4409  unexbOLD  7696  undifixp  8876  unfi  9099  unxpdom  9163  ackbij1lem16  10150  fin23lem28  10256  ttukeylem6  10430  lcmfun  16608  ipodrsima  18501  mplsubglem  21990  mretopd  23070  iscldtop  23073  dfconn2  23397  nconnsubb  23401  comppfsc  23510  noextendseq  27648  oncutlt  28273  spanun  31634  constrextdg2lem  33911  locfinref  34004  isros  34331  unelros  34334  difelros  34335  rossros  34343  inelcarsg  34474  fineqvac  35279  rankung  36367  bj-funun  37585  paddval  40261  dochsatshp  41914  nacsfix  43161  eldioph4b  43260  eldioph4i  43261  fiuneneq  43641  isotone1  44496  fiiuncl  45517