Theorem uneq2d 3657

Description: Deduction adding union to the left in a class equality. (Contributed by NM, 29-Mar-1998.)

Hypothesis

Ref	Expression
uneq1d.1

Assertion

Ref	Expression
uneq2d

Proof of Theorem uneq2d

Step	Hyp	Ref	Expression
1		uneq1d.1	. 2
2		uneq2 3651	. 2
3	1, 2	syl 16	1

Syntax hints:  ->wi 4  =wceq 1395  u.cun 3473

This theorem is referenced by:  ifeq2  3946  tpeq3  4120  iununi  4415  relcoi1  5541  resasplit  5760  fvun1  5944  fmptapd  6095  fndifnfp  6100  fvunsn  6103  fnsnsplit  6108  oev2  7192  oarec  7230  ralxpmap  7488  sbthlem5  7651  sbthlem6  7652  domss2  7696  domunfican  7813  fiint  7817  fodomfi  7819  pm54.43  8402  kmlem2  8552  kmlem11  8561  cdaval  8571  cdaassen  8583  ackbij1lem1  8621  fin23lem26  8726  axdc3lem4  8854  fpwwe2lem13  9041  wunex2  9137  wuncval2  9146  snunico  11676  ioojoin  11680  fzsuc  11756  fseq1p1m1  11781  fseq1m1p1  11782  fzosplitsnm1  11890  fzosplitsn  11918  fzosplitprm1  11919  hashfun  12495  s4prop  12863  fsumm1  13566  climcndslem1  13661  fprodm1  13771  ruclem4  13967  vdwap1  14495  setscom  14662  mreexmrid  15040  mreexexlemd  15041  mreexexlem2d  15042  cnvtsr  15852  dprd2da  17091  dmdprdsplit2lem  17094  lspun0  17657  lbsextlem4  17807  cmpcld  19902  comppfsc  20033  trfil2  20388  cldsubg  20609  tsmsresOLD  20645  tsmsres  20646  icccmplem2  21328  uniioombllem4  21995  ppiprm  23425  chtprm  23427  pntrsumbnd2  23752  wwlknext  24724  eupath2lem3  24979  difres  27457  ofpreima2  27508  fzspl  27598  ordtprsuni  27901  ordtcnvNEW  27902  ballotlemfp1  28430  subfacp1lem1  28623  cvmscld  28718  mrsubvrs  28882  mclsval  28923  rankaltopb  29629  rankung  29823  diophren  30747  ioounsn  31177  snunioo2  31544  snunioo1  31552  dvmptfprodlem  31741  stoweidlem11  31793  stoweidlem26  31808  fourierdlem33  31922  fzosplitpr  32342  setsidvald  32557  lmod1zr  33094  bnj941  33831  bnj944  33996  lshpnel2N  34710  paddfval  35521  hdmapval  37558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3480