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 2791	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵))

Syntax hints:   → wi 4   = wceq 1541   ∪ cun 3895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902

This theorem is referenced by:  uneq12  4110  uneq2i  4112  uneq2d  4115  uneqin  4236  disjssun  4415  unexbOLD  7681  undifixp  8858  unfi  9080  unxpdom  9143  ackbij1lem16  10125  fin23lem28  10231  ttukeylem6  10405  lcmfun  16556  ipodrsima  18447  mplsubglem  21936  mretopd  23007  iscldtop  23010  dfconn2  23334  nconnsubb  23338  comppfsc  23447  noextendseq  27606  onscutlt  28201  spanun  31525  constrextdg2lem  33761  locfinref  33854  isros  34181  unelros  34184  difelros  34185  rossros  34193  inelcarsg  34324  fineqvac  35139  rankung  36210  bj-funun  37296  paddval  39907  dochsatshp  41560  nacsfix  42815  eldioph4b  42914  eldioph4i  42915  fiuneneq  43295  isotone1  44151  fiiuncl  45172