Theorem uneq2 3896

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

Syntax hints:   → wi 4   = wceq 1624   ∪ cun 3705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-v 3334  df-un 3712

This theorem is referenced by:  uneq12  3897  uneq2i  3899  uneq2d  3902  uneqin  4013  disjssun  4172  uniprg  4594  unexb  7115  undifixp  8102  unxpdom  8324  ackbij1lem16  9241  fin23lem28  9346  ttukeylem6  9520  lcmfun  15552  ipodrsima  17358  mplsubglem  19628  mretopd  21090  iscldtop  21093  dfconn2  21416  nconnsubb  21420  comppfsc  21529  spanun  28705  locfinref  30209  isros  30532  unelros  30535  difelros  30536  rossros  30544  inelcarsg  30674  noextendseq  32118  rankung  32571  paddval  35579  dochsatshp  37234  nacsfix  37769  eldioph4b  37869  eldioph4i  37870  fiuneneq  38269  isotone1  38840  fiiuncl  39725