Theorem uneq2d 3304

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 3298	. 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 1364   u. cun 3142

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-v 2754  df-un 3148

This theorem is referenced by:  ifeq2  3553  tpeq3  3695  iununir  3985  unisucg  4429  relcoi1  5175  resasplitss  5410  fvun1  5598  fmptapd  5723  fvunsng  5726  fnsnsplitss  5731  tfr1onlemaccex  6367  tfrcllemaccex  6380  rdgeq1  6390  rdgivallem  6400  rdgisuc1  6403  rdgon  6405  rdg0  6406  oav2  6482  oasuc  6483  omv2  6484  omsuc  6491  fnsnsplitdc  6524  unsnfidcex  6937  undifdc  6941  fiintim  6946  ssfirab  6951  fnfi  6954  fidcenumlemr  6972  sbthlemi5  6978  sbthlemi6  6979  pm54.43  7207  fzsuc  10087  fseq1p1m1  10112  fseq1m1p1  10113  fzosplitsnm1  10227  fzosplitsn  10251  fzosplitprm1  10252  resunimafz0  10829  zfz1isolemsplit  10836  fsumm1  11442  fprodm1  11624  ennnfonelemp1  12425  ennnfonelemhdmp1  12428  ennnfonelemkh  12431  ennnfonelemhf1o  12432  ennnfonelemnn0  12441  strsetsid  12513  setscom  12520  lspun0  13702  bj-charfundcALT  14945