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 2823	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵))

Syntax hints:   → wi 4   = wceq 1570   ∪ cun 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910

This theorem is referenced by:  uneq12  4117  uneq2i  4119  uneq2d  4122  uneqin  4242  disjssun  4428  undifixp  8928  unfi  9151  unxpdom  9215  ackbij1lem16  10213  fin23lem28  10319  ttukeylem6  10493  lcmfun  16698  ipodrsima  18592  mplsubglem  22148  mretopd  23249  iscldtop  23252  dfconn2  23576  nconnsubb  23580  comppfsc  23689  noextendseq  27831  oncutlt  28457  spanun  31897  constrextdg2lem  34138  locfinref  34231  isros  34558  unelros  34561  difelros  34562  rossros  34570  inelcarsg  34701  fineqvac  35529  rankung  36658  bj-funun  37916  paddval  40592  dochsatshp  42245  nacsfix  43463  eldioph4b  43558  eldioph4i  43559  fiuneneq  43939  isotone1  44794  fiiuncl  45805