Theorem uneq12d 3644

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 3638	. 2 |- ( ( A = B /\ C = D ) -> ( A u. C ) = ( B u. D ) )
4	1, 2, 3	syl2anc 661	1 |- ( ph -> ( A u. C ) = ( B u. D ) )

Syntax hints:   -> wi 4   = wceq 1383   u. cun 3459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-un 3466

This theorem is referenced by:  csbun  3843  csbungOLD  3844  csbprg  4074  disjpr2  4077  diftpsn3  4153  suceq  4933  rnpropg  5478  fntpg  5633  foun  5824  f1oprswap  5845  fnimapr  5922  residpr  6060  fsnunfv  6096  fsnunres  6097  oarec  7213  ereq1  7320  mapunen  7688  cnfcomlem  8146  cnfcomlemOLD  8154  trcl  8162  r0weon  8393  infxpen  8395  cfsmolem  8653  cfsmo  8654  axdc3lem4  8836  ttukeylem3  8894  ttukey2g  8899  alephadd  8955  fpwwe2lem13  9023  wunex2  9119  wuncval2  9128  inar1  9156  prunioo  11658  fztp  11745  fzsuc2  11746  fseq1p1m1  11761  s4dom  12846  setsvalg  14532  setsid  14550  prdsval  14729  imasval  14785  mreexd  14916  mreexexlemd  14918  ipoval  15658  istsr  15721  gsumzaddlem  16808  pwssplit1  17579  psrval  17885  ordtval  19563  ordtcnv  19575  paste  19668  consuba  19794  ptval2  19975  dfac14  19992  xkoptsub  20028  ptuncnv  20181  ptunhmeo  20182  xpstopnlem1  20183  alexsubALTlem3  20422  ustuqtop1  20617  rrxmvallem  21704  ovolioo  21851  uniiccdif  21860  itgsplitioo  22117  limcfval  22149  lhop2  22289  lgsquadlem2  23502  axlowdimlem13  24129  axlowdimlem15  24131  axlowdim  24136  eengv  24154  constr2spthlem1  24468  constr3pthlem1  24527  constr3pthlem2  24528  vdgrun  24773  vdgrfiun  24774  ex-res  25034  imadifxp  27330  resf1o  27425  ordtprsval  27773  ordtprsuni  27774  ordtcnvNEW  27775  eulerpartlemt  28183  sseqval  28200  probun  28231  cvmliftlem10  28612  mrexval  28734  mrsubffval  28740  msrval  28771  mthmpps  28815  dfrtrcl2  28944  symdifeq1  29445  lineunray  29772  finixpnum  30013  ptrest  30023  mblfinlem2  30027  itg2addnclem2  30042  istopclsd  30607  fzsplit1nn0  30662  diophrw  30667  eldioph2lem1  30668  eldioph2lem2  30669  diophin  30681  diophren  30722  pwssplit4  31010  mendval  31108  iocunico  31154  iunxprg  32140  estrreslem2  32493  xpprsng  32654  mndpsuppss  32699  bnj1373  33819  bnj1489  33845  ldualset  34590  paddval  35262  paddcom  35277  dvafset  36470  dvaset  36471  dvhfset  36547  dvhset  36548  hdmapfval  37297  hlhilset  37404