Theorem uneq12d 3589

Description: Equality deduction for 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 3583	. 2 |- ( ( A = B /\ C = D ) -> ( A u. C ) = ( B u. D ) )
4	1, 2, 3	syl2anc 667	1 |- ( ph -> ( A u. C ) = ( B u. D ) )

Syntax hints:   -> wi 4   = wceq 1444   u. cun 3402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-v 3047  df-un 3409

This theorem is referenced by:  symdifeq1  3665  csbun  3798  csbprg  4031  disjpr2  4034  diftpsn3  4110  rnpropg  5316  suceq  5488  fntpg  5637  foun  5832  f1oprswap  5854  fnimapr  5929  residpr  6068  fsnunfv  6104  fsnunres  6105  oarec  7263  ereq1  7370  mapunen  7741  cnfcomlem  8204  trcl  8212  r0weon  8443  infxpen  8445  cfsmolem  8700  cfsmo  8701  axdc3lem4  8883  ttukeylem3  8941  ttukey2g  8946  alephadd  9002  fpwwe2lem13  9067  wunex2  9163  wuncval2  9172  inar1  9200  prunioo  11761  fztp  11852  fzsuc2  11853  fseq1p1m1  11868  s4dom  13004  trclun  13078  relexp0g  13085  relexpsucnnr  13088  dfrtrcl2  13125  setsvalg  15145  setsid  15164  prdsval  15353  imasval  15411  imasvalOLD  15412  mreexd  15548  mreexexlemd  15550  estrreslem2  16023  ipoval  16400  istsr  16463  gsumzaddlem  17554  pwssplit1  18282  psrval  18586  ordtval  20205  ordtcnv  20217  paste  20310  consuba  20435  ptval2  20616  dfac14  20633  xkoptsub  20669  ptuncnv  20822  ptunhmeo  20823  xpstopnlem1  20824  alexsubALTlem3  21064  ustuqtop1  21256  rrxmvallem  22358  ovolioo  22521  uniiccdif  22535  itgsplitioo  22795  limcfval  22827  lhop2  22967  lgsquadlem2  24283  axlowdimlem13  24984  axlowdimlem15  24986  axlowdim  24991  eengv  25009  constr2spthlem1  25324  constr3pthlem1  25383  constr3pthlem2  25384  vdgrun  25629  vdgrfiun  25630  ex-res  25891  imadifxp  28212  padct  28307  resf1o  28315  ordtprsval  28724  ordtprsuni  28725  ordtcnvNEW  28726  unelcarsg  29144  carsgclctunlem1  29149  eulerpartlemt  29204  sseqval  29221  probun  29252  bnj1373  29839  bnj1489  29865  cvmliftlem10  30017  mrexval  30139  mrsubffval  30145  msrval  30176  mthmpps  30220  lineunray  30914  finixpnum  31930  ptrest  31939  poimirlem1  31941  poimirlem2  31942  poimirlem3  31943  poimirlem4  31944  poimirlem5  31945  poimirlem6  31946  poimirlem7  31947  poimirlem8  31948  poimirlem9  31949  poimirlem10  31950  poimirlem11  31951  poimirlem12  31952  poimirlem15  31955  poimirlem16  31956  poimirlem17  31957  poimirlem18  31958  poimirlem19  31959  poimirlem20  31960  poimirlem21  31961  poimirlem22  31962  poimirlem23  31963  poimirlem24  31964  poimirlem26  31966  poimirlem27  31967  poimirlem28  31968  poimirlem32  31972  mblfinlem2  31978  itg2addnclem2  31994  ldualset  32691  paddval  33363  paddcom  33378  dvafset  34571  dvaset  34572  dvhfset  34648  dvhset  34649  hdmapfval  35398  hlhilset  35505  istopclsd  35542  fzsplit1nn0  35596  diophrw  35601  eldioph2lem1  35602  eldioph2lem2  35603  diophin  35615  diophren  35656  pwssplit4  35947  mendval  36049  iocunico  36095  rclexi  36222  rtrclex  36224  rtrclexi  36228  cnvrcl0  36232  dfrtrcl5  36236  dfrcl2  36266  dfrcl3  36267  iunrelexp0  36294  trclfvdecomr  36320  dfrtrcl4  36330  frege131d  36356  dvmptfprodlem  37819  caratheodorylem1  38347  fzopredsuc  38720  iunxprg  39004  vtxduhgrun  39538  xpprsng  40166  mndpsuppss  40209  aacllem  40593