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  4506  relcoi1  5263  resasplitss  5510  fvun1  5705  fmptapd  5837  fvunsng  5840  fnsnsplitss  5845  tfr1onlemaccex  6505  tfrcllemaccex  6518  rdgeq1  6528  rdgivallem  6538  rdgisuc1  6541  rdgon  6543  rdg0  6544  oav2  6622  oasuc  6623  omv2  6624  omsuc  6631  fnsnsplitdc  6664  unsnfidcex  7098  undifdc  7102  fiintim  7109  ssfirab  7114  fnfi  7119  fidcenumlemr  7138  sbthlemi5  7144  sbthlemi6  7145  pm54.43  7379  fzsuc  10282  fseq1p1m1  10307  fseq1m1p1  10308  fzosplitsnm1  10432  fzosplitsn  10456  fzosplitprm1  10457  resunimafz0  11071  zfz1isolemsplit  11078  fsumm1  11948  fprodm1  12130  ennnfonelemp1  12998  ennnfonelemhdmp1  13001  ennnfonelemkh  13004  ennnfonelemhf1o  13005  ennnfonelemnn0  13014  strsetsid  13086  setscom  13093  lspun0  14410  bj-charfundcALT  16281