Theorem uneq2d 3767

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 3761	. 2 |- ( A = B -> ( C u. A ) = ( C u. B ) )
3	1, 2	syl 17	1 |- ( ph -> ( C u. A ) = ( C u. B ) )

Syntax hints:   -> wi 4   = wceq 1483   u. cun 3572

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579

This theorem is referenced by:  ifeq2  4091  tpeq3  4279  iununi  4610  sucprc  5800  resasplit  6074  fvun1  6269  fmptapd  6437  fndifnfp  6442  fvunsn  6445  fnsnsplit  6450  oev2  7603  oarec  7642  ralxpmap  7907  sbthlem5  8074  sbthlem6  8075  domss2  8119  domunfican  8233  fiint  8237  fodomfi  8239  pm54.43  8826  kmlem2  8973  kmlem11  8982  cdaval  8992  cdaassen  9004  ackbij1lem1  9042  fin23lem26  9147  axdc3lem4  9275  fpwwe2lem13  9464  wunex2  9560  wuncval2  9569  snunico  12299  ioojoin  12303  fzsuc  12388  fseq1p1m1  12414  fseq1m1p1  12415  fzosplitsnm1  12542  fzosplitsn  12576  fzosplitpr  12577  fzosplitprm1  12578  hashfun  13224  resunimafz0  13229  s4prop  13655  fsumm1  14480  climcndslem1  14581  fprodm1  14697  ruclem4  14963  lcmfunsnlem1  15350  lcmfunsnlem2lem1  15351  lcmfunsnlem2lem2  15352  lcmfunsnlem2  15353  lcmfunsn  15357  vdwap1  15681  setsidvald  15889  setscom  15903  mreexmrid  16303  mreexexlemd  16304  mreexexlem2d  16305  cnvtsr  17222  dprd2da  18441  dmdprdsplit2lem  18444  lspun0  19011  lbsextlem4  19161  cmpcld  21205  comppfsc  21335  trfil2  21691  cldsubg  21914  tsmsres  21947  icccmplem2  22626  uniioombllem4  23354  ppiprm  24877  chtprm  24879  pntrsumbnd2  25256  pthdlem1  26662  wwlksnext  26788  numclwwlkovf2exlem1  27211  difres  29413  ofpreima2  29466  fzspl  29550  ordtprsuni  29965  ordtcnvNEW  29966  carsgsigalem  30377  ballotlemfp1  30553  fsum2dsub  30685  reprsuc  30693  bnj941  30843  bnj944  31008  subfacp1lem1  31161  cvmscld  31255  mrsubvrs  31419  mclsval  31460  noextend  31819  nodenselem5  31838  nosupbnd2lem1  31861  rankaltopb  32086  rankung  32273  lindsenlbs  33404  poimirlem1  33410  poimirlem2  33411  poimirlem4  33413  poimirlem6  33415  poimirlem7  33416  poimirlem8  33417  poimirlem13  33422  poimirlem14  33423  poimirlem16  33425  poimirlem17  33426  poimirlem18  33427  poimirlem19  33428  poimirlem20  33429  poimirlem21  33430  poimirlem22  33431  poimirlem26  33435  poimirlem28  33437  poimirlem31  33440  poimirlem32  33441  lshpnel2N  34272  paddfval  35083  hdmapval  37120  diophren  37377  ioounsn  37795  iunrelexp0  37994  trclfvdecoml  38021  isotone1  38346  iunp1  39235  snunioo2  39731  snunioo1  39738  dvmptfprodlem  40159  stoweidlem11  40228  stoweidlem26  40243  fourierdlem33  40357  fzopredsuc  41333  iccpartltu  41361  iccpartgt  41363  lmod1zr  42282