Theorem uneq2 4137

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

Syntax hints:   → wi 4   = wceq 1540   ∪ cun 3924

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931

This theorem is referenced by:  uneq12  4138  uneq2i  4140  uneq2d  4143  uneqin  4264  disjssun  4443  unexbOLD  7740  undifixp  8946  unfi  9183  unxpdom  9259  ackbij1lem16  10246  fin23lem28  10352  ttukeylem6  10526  lcmfun  16662  ipodrsima  18549  mplsubglem  21957  mretopd  23028  iscldtop  23031  dfconn2  23355  nconnsubb  23359  comppfsc  23468  noextendseq  27629  spanun  31472  constrextdg2lem  33728  locfinref  33818  isros  34145  unelros  34148  difelros  34149  rossros  34157  inelcarsg  34289  fineqvac  35074  rankung  36130  bj-funun  37216  paddval  39763  dochsatshp  41416  nacsfix  42682  eldioph4b  42781  eldioph4i  42782  fiuneneq  43163  isotone1  44019  fiiuncl  45037