Theorem uneq2d 3169

Description: Deduction adding union to the left in a class equality. (Contributed by NM, 29-Mar-1998.)

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 3163	. 2 |- ( A = B -> ( C u. A ) = ( C u. B ) )
3	1, 2	syl 14	1 |- ( ph -> ( C u. A ) = ( C u. B ) )

Syntax hints:   -> wi 4   = wceq 1296   u. cun 3011

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-v 2635  df-un 3017

This theorem is referenced by:  ifeq2  3417  tpeq3  3550  iununir  3834  unisucg  4265  relcoi1  4996  resasplitss  5225  fvun1  5405  fmptapd  5527  fvunsng  5530  fnsnsplitss  5535  tfr1onlemaccex  6151  tfrcllemaccex  6164  rdgeq1  6174  rdgivallem  6184  rdgisuc1  6187  rdgon  6189  rdg0  6190  oav2  6264  oasuc  6265  omv2  6266  omsuc  6273  fnsnsplitdc  6304  unsnfidcex  6710  undifdc  6714  fiintim  6719  ssfirab  6723  fnfi  6726  fidcenumlemr  6744  sbthlemi5  6750  sbthlemi6  6751  pm54.43  6915  fzsuc  9632  fseq1p1m1  9657  fseq1m1p1  9658  fzosplitsnm1  9769  fzosplitsn  9793  fzosplitprm1  9794  resunimafz0  10367  zfz1isolemsplit  10374  fsumm1  10975  strsetsid  11692  setscom  11699