Theorem uneq2 4116

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911

This theorem is used by:  uneq12  4117  uneq2i  4119  uneq2d  4122  uneqin  4242  disjssun  4428  undifixp  8938  unfi  9162  unxpdom  9226  ackbij1lem16  10233  fin23lem28  10339  ttukeylem6  10513  lcmfun  16727  ipodrsima  18621  mplsubglem  22200  mretopd  23301  iscldtop  23304  dfconn2  23628  nconnsubb  23632  comppfsc  23742  noextendseq  27884  oncutlt  28510  spanun  31970  constrextdg2lem  34204  locfinref  34297  isros  34625  unelros  34628  difelros  34629  rossros  34637  inelcarsg  34768  fineqvac  35588  rankung  36697  bj-funun  37955  paddval  40632  dochsatshp  42285  nacsfix  43503  eldioph4b  43598  eldioph4i  43599  fiuneneq  43979  isotone1  44834  fiiuncl  45845