Theorem uneq2 4133

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

Syntax hints:   → wi 4   = wceq 1533   ∪ cun 3934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3497  df-un 3941

This theorem is referenced by:  uneq12  4134  uneq2i  4136  uneq2d  4139  uneqin  4255  disjssun  4417  uniprg  4846  unexb  7465  undifixp  8492  unxpdom  8719  ackbij1lem16  9651  fin23lem28  9756  ttukeylem6  9930  lcmfun  15983  ipodrsima  17769  mplsubglem  20208  mretopd  21694  iscldtop  21697  dfconn2  22021  nconnsubb  22025  comppfsc  22134  spanun  29316  locfinref  31100  isros  31422  unelros  31425  difelros  31426  rossros  31434  inelcarsg  31564  noextendseq  33169  rankung  33622  bj-funun  34528  paddval  36928  dochsatshp  38581  nacsfix  39302  eldioph4b  39401  eldioph4i  39402  fiuneneq  39790  isotone1  40391  fiiuncl  41320