Theorem uneq2 4185

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

Syntax hints:   → wi 4   = wceq 1537   ∪ cun 3974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981

This theorem is referenced by:  uneq12  4186  uneq2i  4188  uneq2d  4191  uneqin  4308  disjssun  4491  unexbOLD  7783  undifixp  8992  unfi  9238  unxpdom  9316  ackbij1lem16  10303  fin23lem28  10409  ttukeylem6  10583  lcmfun  16692  ipodrsima  18611  mplsubglem  22042  mretopd  23121  iscldtop  23124  dfconn2  23448  nconnsubb  23452  comppfsc  23561  noextendseq  27730  spanun  31577  locfinref  33787  isros  34132  unelros  34135  difelros  34136  rossros  34144  inelcarsg  34276  fineqvac  35073  rankung  36130  bj-funun  37218  paddval  39755  dochsatshp  41408  nacsfix  42668  eldioph4b  42767  eldioph4i  42768  fiuneneq  43153  isotone1  44010  fiiuncl  44967