Theorem uneq2 4158

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954

This theorem is referenced by:  uneq12  4159  uneq2i  4161  uneq2d  4164  uneqin  4279  disjssun  4468  uniprgOLD  4929  unexb  7735  undifixp  8928  unfi  9172  unxpdom  9253  ackbij1lem16  10230  fin23lem28  10335  ttukeylem6  10509  lcmfun  16582  ipodrsima  18494  mplsubglem  21558  mretopd  22596  iscldtop  22599  dfconn2  22923  nconnsubb  22927  comppfsc  23036  noextendseq  27170  spanun  30798  locfinref  32821  isros  33166  unelros  33169  difelros  33170  rossros  33178  inelcarsg  33310  fineqvac  34097  rankung  35138  bj-funun  36133  paddval  38669  dochsatshp  40322  nacsfix  41450  eldioph4b  41549  eldioph4i  41550  fiuneneq  41939  isotone1  42799  fiiuncl  43752