Theorem uneq2d 3358

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 3352	. 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 1395   u. cun 3195

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201

This theorem is referenced by:  ifeq2  3606  tpeq3  3754  iununir  4049  unisucg  4505  relcoi1  5260  resasplitss  5505  fvun1  5700  fmptapd  5830  fvunsng  5833  fnsnsplitss  5838  tfr1onlemaccex  6494  tfrcllemaccex  6507  rdgeq1  6517  rdgivallem  6527  rdgisuc1  6530  rdgon  6532  rdg0  6533  oav2  6609  oasuc  6610  omv2  6611  omsuc  6618  fnsnsplitdc  6651  unsnfidcex  7082  undifdc  7086  fiintim  7093  ssfirab  7098  fnfi  7103  fidcenumlemr  7122  sbthlemi5  7128  sbthlemi6  7129  pm54.43  7363  fzsuc  10265  fseq1p1m1  10290  fseq1m1p1  10291  fzosplitsnm1  10415  fzosplitsn  10439  fzosplitprm1  10440  resunimafz0  11053  zfz1isolemsplit  11060  fsumm1  11927  fprodm1  12109  ennnfonelemp1  12977  ennnfonelemhdmp1  12980  ennnfonelemkh  12983  ennnfonelemhf1o  12984  ennnfonelemnn0  12993  strsetsid  13065  setscom  13072  lspun0  14389  bj-charfundcALT  16172