Theorem uneq2d 3375

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 3369	. 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 1398   u. cun 3211

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3217

This theorem is referenced by:  ifeq2  3628  tpeq3  3781  iununir  4077  unisucg  4537  relcoi1  5296  resasplitss  5546  fvun1  5745  fmptapd  5877  fvunsng  5880  fnsnsplitss  5885  tfr1onlemaccex  6581  tfrcllemaccex  6594  rdgeq1  6604  rdgivallem  6614  rdgisuc1  6617  rdgon  6619  rdg0  6620  oav2  6698  oasuc  6699  omv2  6700  omsuc  6707  fnsnsplitdc  6740  unsnfidcex  7182  undifdc  7186  fiintim  7193  ssfirab  7199  fnfi  7205  fidcenumlemr  7227  sbthlemi5  7233  sbthlemi6  7234  pm54.43  7489  fzsuc  10406  fzspl  10407  fseq1p1m1  10432  fseq1m1p1  10433  fzosplitsnm1  10558  fzosplitsn  10582  fzosplitpr  10583  fzosplitprm1  10584  resunimafz0  11202  zfz1isolemsplit  11214  fsumm1  12106  fprodm1  12288  ballotfilemfp1  13152  ennnfonelemp1  13174  ennnfonelemhdmp1  13177  ennnfonelemkh  13180  ennnfonelemhf1o  13181  ennnfonelemnn0  13190  strsetsid  13262  setscom  13269  lspun0  14590  p1evtxdeqfilem  16323  clwwlknonex2lem1  16449  bj-charfundcALT  16596  gfsump1  16885