Theorem uneq2 4109

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

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

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 2147  ax-9 2155  ax-ext 2733

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 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904

This theorem is used by:  uneq12  4110  uneq2i  4112  uneq2d  4115  uneqin  4235  disjssun  4421  undifixp  8962  unfi  9186  unxpdom  9250  rankung  9873  ackbij1lem16  10312  fin23lem28  10418  ttukeylem6  10592  lcmfun  16820  ipodrsima  18715  mplsubglem  22306  mretopd  23410  iscldtop  23413  dfconn2  23737  nconnsubb  23741  comppfsc  23851  noextendseq  28024  oncutlt  28650  spanun  32147  constrextdg2lem  34380  locfinref  34473  isros  34801  unelros  34804  difelros  34805  rossros  34813  inelcarsg  34943  fineqvac  35784  bj-funun  38173  paddval  40855  dochsatshp  42508  nacsfix  43722  eldioph4b  43817  eldioph4i  43818  fiuneneq  44193  isotone1  45047  fiiuncl  46081