Theorem uneq2d 2187

Description: Deduction adding union to the left in a class equality.

Hypothesis

Ref	Expression
uneq1d.1	⊢ (φ → A = B)

Assertion

Ref	Expression
uneq2d	⊢ (φ → (C ∪ A) = (C ∪ B))

Proof of Theorem uneq2d

Step	Hyp	Ref	Expression
1		uneq1d.1	. 2 ⊢ (φ → A = B)
2		uneq2 2181	. 2 ⊢ (A = B → (C ∪ A) = (C ∪ B))
3	1, 2	syl 10	1 ⊢ (φ → (C ∪ A) = (C ∪ B))

Syntax hints:   → wi 3   = wceq 958   ∪ cun 2048

This theorem is referenced by:  uneq12d 2188  suceq 3040  oev2 4168  oarec 4202  sbthlem5 4457  sbthlem6 4458  mapunen 4508  unifiOLD 4570  fiint 4572  fiintOLD 4573  fodomfi 4575  fodomfiOLD 4576  pm54.43 4581  kmlem2 4776  kmlem11 4785  cdavalt 4931  icoun 6414  snunioo 6416  ioojoint 6417

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-v 1815  df-un 2053

Copyright terms: Public domain