Theorem uneq2 4087

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888

This theorem is referenced by:  uneq12  4088  uneq2i  4090  uneq2d  4093  uneqin  4209  disjssun  4398  uniprgOLD  4856  unexb  7576  undifixp  8680  unfi  8917  unxpdom  8959  ackbij1lem16  9922  fin23lem28  10027  ttukeylem6  10201  lcmfun  16278  ipodrsima  18174  mplsubglem  21115  mretopd  22151  iscldtop  22154  dfconn2  22478  nconnsubb  22482  comppfsc  22591  spanun  29808  locfinref  31693  isros  32036  unelros  32039  difelros  32040  rossros  32048  inelcarsg  32178  fineqvac  32966  noextendseq  33797  rankung  34395  bj-funun  35350  paddval  37739  dochsatshp  39392  nacsfix  40450  eldioph4b  40549  eldioph4i  40550  fiuneneq  40938  isotone1  41547  fiiuncl  42502