Theorem uneq12d 3580

Description: Equality deduction for the union of two classes. (Contributed by NM, 29-Sep-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)

Hypotheses

Ref	Expression
uneq1d.1	|- ( ph -> A = B )
uneq12d.2	|- ( ph -> C = D )

Assertion

Ref	Expression
uneq12d	|- ( ph -> ( A u. C ) = ( B u. D ) )

Proof of Theorem uneq12d

Step	Hyp	Ref	Expression
1		uneq1d.1	. 2 |- ( ph -> A = B )
2		uneq12d.2	. 2 |- ( ph -> C = D )
3		uneq12 3574	. 2 |- ( ( A = B /\ C = D ) -> ( A u. C ) = ( B u. D ) )
4	1, 2, 3	syl2anc 673	1 |- ( ph -> ( A u. C ) = ( B u. D ) )

Syntax hints:   -> wi 4   = wceq 1452   u. cun 3388

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-un 3395

This theorem is referenced by:  symdifeq1  3656  csbun  3802  csbprg  4022  disjpr2  4025  diftpsn3  4101  iunxprg  4356  rnpropg  5323  suceq  5495  fntpg  5644  foun  5846  f1oprswap  5868  fnimapr  5944  residpr  6084  fsnunfv  6120  fsnunres  6121  oarec  7281  ereq1  7388  mapunen  7759  cnfcomlem  8222  trcl  8230  r0weon  8461  infxpen  8463  cfsmolem  8718  cfsmo  8719  axdc3lem4  8901  ttukeylem3  8959  ttukey2g  8964  alephadd  9020  fpwwe2lem13  9085  wunex2  9181  wuncval2  9190  inar1  9218  prunioo  11787  fztp  11878  fzsuc2  11879  fseq1p1m1  11894  s3tpop  13063  s4dom  13073  trclun  13155  relexp0g  13162  relexpsucnnr  13165  dfrtrcl2  13202  setsvalg  15223  setsid  15242  prdsval  15431  imasval  15489  imasvalOLD  15490  mreexd  15626  mreexexlemd  15628  estrreslem2  16101  ipoval  16478  istsr  16541  gsumzaddlem  17632  pwssplit1  18360  psrval  18663  ordtval  20282  ordtcnv  20294  paste  20387  consuba  20512  ptval2  20693  dfac14  20710  xkoptsub  20746  ptuncnv  20899  ptunhmeo  20900  xpstopnlem1  20901  alexsubALTlem3  21142  ustuqtop1  21334  rrxmvallem  22436  ovolioo  22600  uniiccdif  22614  itgsplitioo  22874  limcfval  22906  lhop2  23046  lgsquadlem2  24362  axlowdimlem13  25063  axlowdimlem15  25065  axlowdim  25070  eengv  25088  constr2spthlem1  25403  constr3pthlem1  25462  constr3pthlem2  25463  vdgrun  25708  vdgrfiun  25709  ex-res  25970  imadifxp  28288  padct  28382  resf1o  28390  ordtprsval  28798  ordtprsuni  28799  ordtcnvNEW  28800  unelcarsg  29217  carsgclctunlem1  29222  eulerpartlemt  29277  sseqval  29294  probun  29325  bnj1373  29911  bnj1489  29937  cvmliftlem10  30089  mrexval  30211  mrsubffval  30217  msrval  30248  mthmpps  30292  lineunray  30985  finixpnum  31994  ptrest  32003  poimirlem1  32005  poimirlem2  32006  poimirlem3  32007  poimirlem4  32008  poimirlem5  32009  poimirlem6  32010  poimirlem7  32011  poimirlem8  32012  poimirlem9  32013  poimirlem10  32014  poimirlem11  32015  poimirlem12  32016  poimirlem15  32019  poimirlem16  32020  poimirlem17  32021  poimirlem18  32022  poimirlem19  32023  poimirlem20  32024  poimirlem21  32025  poimirlem22  32026  poimirlem23  32027  poimirlem24  32028  poimirlem26  32030  poimirlem27  32031  poimirlem28  32032  poimirlem32  32036  mblfinlem2  32042  itg2addnclem2  32058  ldualset  32762  paddval  33434  paddcom  33449  dvafset  34642  dvaset  34643  dvhfset  34719  dvhset  34720  hdmapfval  35469  hlhilset  35576  istopclsd  35613  fzsplit1nn0  35667  diophrw  35672  eldioph2lem1  35673  eldioph2lem2  35674  diophin  35686  diophren  35727  pwssplit4  36018  mendval  36120  iocunico  36166  rclexi  36293  rtrclex  36295  rtrclexi  36299  cnvrcl0  36303  dfrtrcl5  36307  dfrcl2  36337  dfrcl3  36338  iunrelexp0  36365  trclfvdecomr  36391  dfrtrcl4  36401  frege131d  36427  dvmptfprodlem  37916  caratheodorylem1  38466  ovnsubadd2lem  38585  ovolval4lem1  38589  fzopredsuc  38865  vtxdun  39704  trlsegvdeg  40139  xpprsng  40621  mndpsuppss  40664  aacllem  41046