Theorem uneq2d 3313

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 3307	. 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 3151

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 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3157

This theorem is referenced by:  ifeq2  3561  tpeq3  3706  iununir  3996  unisucg  4445  relcoi1  5197  resasplitss  5433  fvun1  5623  fmptapd  5749  fvunsng  5752  fnsnsplitss  5757  tfr1onlemaccex  6401  tfrcllemaccex  6414  rdgeq1  6424  rdgivallem  6434  rdgisuc1  6437  rdgon  6439  rdg0  6440  oav2  6516  oasuc  6517  omv2  6518  omsuc  6525  fnsnsplitdc  6558  unsnfidcex  6976  undifdc  6980  fiintim  6985  ssfirab  6990  fnfi  6995  fidcenumlemr  7014  sbthlemi5  7020  sbthlemi6  7021  pm54.43  7250  fzsuc  10135  fseq1p1m1  10160  fseq1m1p1  10161  fzosplitsnm1  10276  fzosplitsn  10300  fzosplitprm1  10301  resunimafz0  10902  zfz1isolemsplit  10909  fsumm1  11559  fprodm1  11741  ennnfonelemp1  12563  ennnfonelemhdmp1  12566  ennnfonelemkh  12569  ennnfonelemhf1o  12570  ennnfonelemnn0  12579  strsetsid  12651  setscom  12658  lspun0  13921  bj-charfundcALT  15301