Theorem uneq2 4164

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∪ cun 4152

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154

This theorem is used by:  uneq12  4165  uneq2i  4167  uneq2d  4170  uneqin  4237  disjssun  4424  undifixp  9000  unfi  9224  unxpdom  9288  rankung  9910  ackbij1lem16  10351  fin23lem28  10457  ttukeylem6  10631  lcmfun  16864  ipodrsima  18765  mplsubglem  22361  mretopd  23465  iscldtop  23468  dfconn2  23792  nconnsubb  23796  comppfsc  23906  noextendseq  28081  oncutlt  28707  spanun  32204  constrextdg2lem  34491  locfinref  34584  isros  34912  unelros  34915  difelros  34916  rossros  34924  inelcarsg  35054  fineqvac  35925  bj-funun  38441  paddval  41121  dochsatshp  42774  nacsfix  43989  eldioph4b  44084  eldioph4i  44085  fiuneneq  44455  isotone1  45309  fiiuncl  46356