Theorem uneq2 4102

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

Syntax hints:   → wi 4   = wceq 1542   ∪ cun 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894

This theorem is referenced by:  uneq12  4103  uneq2i  4105  uneq2d  4108  uneqin  4229  disjssun  4408  unexbOLD  7702  undifixp  8882  unfi  9105  unxpdom  9169  ackbij1lem16  10156  fin23lem28  10262  ttukeylem6  10436  lcmfun  16614  ipodrsima  18507  mplsubglem  21977  mretopd  23057  iscldtop  23060  dfconn2  23384  nconnsubb  23388  comppfsc  23497  noextendseq  27631  oncutlt  28256  spanun  31616  constrextdg2lem  33892  locfinref  33985  isros  34312  unelros  34315  difelros  34316  rossros  34324  inelcarsg  34455  fineqvac  35260  rankung  36348  bj-funun  37566  paddval  40244  dochsatshp  41897  nacsfix  43144  eldioph4b  43239  eldioph4i  43240  fiuneneq  43620  isotone1  44475  fiiuncl  45496