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 2820	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 2732

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 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904

This theorem is used by:  uneq12  4110  uneq2i  4112  uneq2d  4115  uneqin  4235  disjssun  4421  undifixp  8942  unfi  9166  unxpdom  9230  ackbij1lem16  10237  fin23lem28  10343  ttukeylem6  10517  lcmfun  16736  ipodrsima  18630  mplsubglem  22214  mretopd  23318  iscldtop  23321  dfconn2  23645  nconnsubb  23649  comppfsc  23759  noextendseq  27904  oncutlt  28530  spanun  32027  constrextdg2lem  34259  locfinref  34352  isros  34680  unelros  34683  difelros  34684  rossros  34692  inelcarsg  34823  fineqvac  35643  rankung  36747  bj-funun  38005  paddval  40672  dochsatshp  42325  nacsfix  43558  eldioph4b  43653  eldioph4i  43654  fiuneneq  44034  isotone1  44889  fiiuncl  45900