Theorem uneq2 4156

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

Syntax hints:   → wi 4   = wceq 1534   ∪ cun 3945

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3473  df-un 3952

This theorem is referenced by:  uneq12  4157  uneq2i  4159  uneq2d  4162  uneqin  4279  disjssun  4468  uniprgOLD  4927  unexb  7750  undifixp  8953  unfi  9197  unxpdom  9278  ackbij1lem16  10259  fin23lem28  10364  ttukeylem6  10538  lcmfun  16616  ipodrsima  18533  mplsubglem  21941  mretopd  23009  iscldtop  23012  dfconn2  23336  nconnsubb  23340  comppfsc  23449  noextendseq  27613  spanun  31368  locfinref  33442  isros  33787  unelros  33790  difelros  33791  rossros  33799  inelcarsg  33931  fineqvac  34717  rankung  35762  bj-funun  36731  paddval  39271  dochsatshp  40924  nacsfix  42132  eldioph4b  42231  eldioph4i  42232  fiuneneq  42620  isotone1  43478  fiiuncl  44429