Theorem uneq2d 2236

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

Hypothesis

Ref	Expression
uneq1d.1	|- (ph -> A = B)

Assertion

Ref	Expression
uneq2d	|- (ph -> (C u. A) = (C u. B))

Proof of Theorem uneq2d

Step	Hyp	Ref	Expression
1		uneq1d.1	. 2 |- (ph -> A = B)
2		uneq2 2230	. 2 |- (A = B -> (C u. A) = (C u. B))
3	1, 2	syl 10	1 |- (ph -> (C u. A) = (C u. B))

Syntax hints:   -> wi 3   = wceq 992   u. cun 2097

This theorem is referenced by:  uneq12d 2237  suceq 3038  oev2 4298  oarec 4332  ac6sfilem2 4589  sbthlem5 4596  sbthlem6 4597  mapunen 4649  unifi 4701  fiint 4703  fodomfi 4709  pm54.43 4715  kmlem2 4912  kmlem11 4921  cdaval 5069  icoun 6540  snunioo 6542  ioojoin 6543  finsschain 11425  cptclsscpt 11489  comppfsc 11578  fbssint 11626  extbas2 11642  filssufil 11656  filmapf 11688  fsum00 11883

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-v 1858  df-un 2102

Copyright terms: Public domain