Theorem uneq2 4135

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-v 3459  df-un 3929

This theorem is referenced by:  uneq12  4136  uneq2i  4138  uneq2d  4141  uneqin  4262  disjssun  4441  unexbOLD  7736  undifixp  8942  unfi  9179  unxpdom  9255  ackbij1lem16  10240  fin23lem28  10346  ttukeylem6  10520  lcmfun  16649  ipodrsima  18536  mplsubglem  21944  mretopd  23015  iscldtop  23018  dfconn2  23342  nconnsubb  23346  comppfsc  23455  noextendseq  27615  spanun  31458  constrextdg2lem  33698  locfinref  33780  isros  34107  unelros  34110  difelros  34111  rossros  34119  inelcarsg  34251  fineqvac  35049  rankung  36105  bj-funun  37191  paddval  39738  dochsatshp  41391  nacsfix  42660  eldioph4b  42759  eldioph4i  42760  fiuneneq  43141  isotone1  43997  fiiuncl  45016