Theorem uneq12d 3618

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

Syntax hints:   -> wi 4   = wceq 1437   u. cun 3431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-v 3080  df-un 3438

This theorem is referenced by:  symdifeq1  3692  csbun  3823  csbprg  4053  disjpr2  4056  diftpsn3  4132  rnpropg  5327  suceq  5498  fntpg  5647  foun  5840  f1oprswap  5861  fnimapr  5936  residpr  6074  fsnunfv  6110  fsnunres  6111  oarec  7262  ereq1  7369  mapunen  7738  cnfcomlem  8194  trcl  8202  r0weon  8433  infxpen  8435  cfsmolem  8689  cfsmo  8690  axdc3lem4  8872  ttukeylem3  8930  ttukey2g  8935  alephadd  8991  fpwwe2lem13  9056  wunex2  9152  wuncval2  9161  inar1  9189  prunioo  11748  fztp  11839  fzsuc2  11840  fseq1p1m1  11855  s4dom  12972  trclun  13046  relexp0g  13053  relexpsucnnr  13056  dfrtrcl2  13093  setsvalg  15097  setsid  15116  prdsval  15305  imasval  15361  mreexd  15492  mreexexlemd  15494  estrreslem2  15967  ipoval  16344  istsr  16407  gsumzaddlem  17482  pwssplit1  18210  psrval  18514  ordtval  20129  ordtcnv  20141  paste  20234  consuba  20359  ptval2  20540  dfac14  20557  xkoptsub  20593  ptuncnv  20746  ptunhmeo  20747  xpstopnlem1  20748  alexsubALTlem3  20988  ustuqtop1  21180  rrxmvallem  22244  ovolioo  22395  uniiccdif  22409  itgsplitioo  22669  limcfval  22701  lhop2  22841  lgsquadlem2  24143  axlowdimlem13  24827  axlowdimlem15  24829  axlowdim  24834  eengv  24852  constr2spthlem1  25166  constr3pthlem1  25225  constr3pthlem2  25226  vdgrun  25471  vdgrfiun  25472  ex-res  25733  imadifxp  28048  padct  28147  resf1o  28155  ordtprsval  28560  ordtprsuni  28561  ordtcnvNEW  28562  unelcarsg  28970  carsgclctunlem1  28975  eulerpartlemt  29027  sseqval  29044  probun  29075  bnj1373  29624  bnj1489  29650  cvmliftlem10  29802  mrexval  29924  mrsubffval  29930  msrval  29961  mthmpps  30005  lineunray  30696  finixpnum  31634  ptrest  31643  poimirlem1  31645  poimirlem2  31646  poimirlem3  31647  poimirlem4  31648  poimirlem5  31649  poimirlem6  31650  poimirlem7  31651  poimirlem8  31652  poimirlem9  31653  poimirlem10  31654  poimirlem11  31655  poimirlem12  31656  poimirlem15  31659  poimirlem16  31660  poimirlem17  31661  poimirlem18  31662  poimirlem19  31663  poimirlem20  31664  poimirlem21  31665  poimirlem22  31666  poimirlem23  31667  poimirlem24  31668  poimirlem26  31670  poimirlem27  31671  poimirlem28  31672  poimirlem32  31676  mblfinlem2  31682  itg2addnclem2  31698  ldualset  32400  paddval  33072  paddcom  33087  dvafset  34280  dvaset  34281  dvhfset  34357  dvhset  34358  hdmapfval  35107  hlhilset  35214  istopclsd  35251  fzsplit1nn0  35305  diophrw  35310  eldioph2lem1  35311  eldioph2lem2  35312  diophin  35324  diophren  35365  pwssplit4  35657  mendval  35752  iocunico  35798  dfrcl2  35909  dfrcl3  35910  iunrelexp0  35937  trclfvdecomr  35963  dfrtrcl4  35973  frege131d  35999  dvmptfprodlem  37392  caratheodorylem1  37860  fzopredsuc  38123  iunxprg  38392  xpprsng  38886  mndpsuppss  38929  aacllem  39314