Theorem uneq12d 3730

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	⊢ (𝜑 → 𝐴 = 𝐵)
uneq12d.2	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
uneq12d	⊢ (𝜑 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))

Proof of Theorem uneq12d

Step	Hyp	Ref	Expression
1		uneq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		uneq12d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
3		uneq12 3724	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))
4	1, 2, 3	syl2anc 691	1 ⊢ (𝜑 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))

Syntax hints:   → wi 4   = wceq 1475   ∪ cun 3538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545

This theorem is referenced by:  symdifeq1  3808  csbun  3961  csbprg  4191  disjpr2  4194  disjpr2OLD  4195  diftpsn3  4273  diftpsn3OLD  4274  iunxprg  4543  rnpropg  5533  suceq  5707  fntpg  5862  foun  6068  f1oprswap  6092  fnimapr  6172  residpr  6315  fsnunfv  6358  fsnunres  6359  oarec  7529  ereq1  7636  mapunen  8014  cnfcomlem  8479  trcl  8487  r0weon  8718  infxpen  8720  cfsmolem  8975  cfsmo  8976  axdc3lem4  9158  ttukeylem3  9216  ttukey2g  9221  alephadd  9278  fpwwe2lem13  9343  wunex2  9439  wuncval2  9448  inar1  9476  prunioo  12172  fztp  12267  fzsuc2  12268  fseq1p1m1  12283  s3tpop  13504  s4dom  13514  trclun  13603  relexp0g  13610  relexpsucnnr  13613  dfrtrcl2  13650  setsvalg  15719  setsdm  15724  setsfun0  15726  setsid  15742  prdsval  15938  imasval  15994  mreexd  16125  mreexexlemd  16127  estrreslem2  16601  ipoval  16977  istsr  17040  gsumzaddlem  18144  pwssplit1  18880  psrval  19183  ordtval  20803  ordtcnv  20815  paste  20908  consuba  21033  ptval2  21214  dfac14  21231  xkoptsub  21267  ptuncnv  21420  ptunhmeo  21421  xpstopnlem1  21422  alexsubALTlem3  21663  ustuqtop1  21855  rrxmvallem  22995  ovolioo  23143  uniiccdif  23152  itgsplitioo  23410  limcfval  23442  lhop2  23582  lgsquadlem2  24906  axlowdimlem13  25634  axlowdimlem15  25636  axlowdim  25641  eengv  25659  constr2spthlem1  26124  constr3pthlem1  26183  constr3pthlem2  26184  vdgrun  26428  vdgrfiun  26429  ex-res  26690  imadifxp  28796  padct  28885  resf1o  28893  ordtprsval  29292  ordtprsuni  29293  ordtcnvNEW  29294  unelcarsg  29701  carsgclctunlem1  29706  eulerpartlemt  29760  sseqval  29777  probun  29808  bnj1373  30352  bnj1489  30378  cvmliftlem10  30530  mrexval  30652  mrsubffval  30658  msrval  30689  mthmpps  30733  lineunray  31424  finixpnum  32564  ptrest  32578  poimirlem1  32580  poimirlem2  32581  poimirlem3  32582  poimirlem4  32583  poimirlem5  32584  poimirlem6  32585  poimirlem7  32586  poimirlem8  32587  poimirlem9  32588  poimirlem10  32589  poimirlem11  32590  poimirlem12  32591  poimirlem15  32594  poimirlem16  32595  poimirlem17  32596  poimirlem18  32597  poimirlem19  32598  poimirlem20  32599  poimirlem21  32600  poimirlem22  32601  poimirlem23  32602  poimirlem24  32603  poimirlem26  32605  poimirlem27  32606  poimirlem28  32607  poimirlem32  32611  mblfinlem2  32617  itg2addnclem2  32632  ldualset  33430  paddval  34102  paddcom  34117  dvafset  35310  dvaset  35311  dvhfset  35387  dvhset  35388  hdmapfval  36137  hlhilset  36244  istopclsd  36281  fzsplit1nn0  36335  diophrw  36340  eldioph2lem1  36341  eldioph2lem2  36342  diophin  36354  diophren  36395  pwssplit4  36677  mendval  36772  iocunico  36815  rclexi  36941  rtrclex  36943  rtrclexi  36947  cnvrcl0  36951  dfrtrcl5  36955  dfrcl2  36985  dfrcl3  36986  iunrelexp0  37013  trclfvdecomr  37039  dfrtrcl4  37049  frege131d  37075  clsk3nimkb  37358  clsk1indlem3  37361  clsk1independent  37364  ntrclskb  37387  ntrclsk3  37388  ntrclsk13  37389  dvmptfprodlem  38834  caratheodorylem1  39416  ovnsubadd2lem  39535  ovolval4lem1  39539  fzopredsuc  39946  vtxdun  40696  trlsegvdeg  41395  xpprsng  41903  mndpsuppss  41946  aacllem  42356