Theorem uneq12d 4132

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 4126	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐷))

Syntax hints:   → wi 4   = wceq 1540   ∪ cun 3912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919

This theorem is referenced by:  symdifeq1  4218  csbun  4404  csbprg  4673  disjpr2  4677  diftpsn3  4766  iunxprg  5060  relresdm1  6004  rnpropg  6195  suceqd  6399  fntpg  6576  foun  6818  f1oprswap  6844  fnimapr  6944  fnimatpd  6945  xpprsng  7112  residpr  7115  fvsnun2  7157  fsnunfv  7161  fsnunres  7162  f1ounsn  7247  f1ofvswap  7281  xpord2pred  8124  xpord3pred  8131  frrlem12  8276  oarec  8526  ereq1  8678  mapunen  9110  cnfcomlem  9652  trcl  9681  djueq12  9857  r0weon  9965  infxpen  9967  cfsmolem  10223  cfsmo  10224  axdc3lem4  10406  ttukeylem3  10464  ttukey2g  10469  alephadd  10530  fpwwe2lem12  10595  wunex2  10691  wuncval2  10700  inar1  10728  prunioo  13442  fztp  13541  fzsuc2  13543  fseq1p1m1  13559  s3tpop  14875  s4dom  14885  s2rn  14929  s3rn  14930  s7rn  14931  trclun  14980  relexp0g  14988  relexpsucnnr  14991  dfrtrcl2  15028  setsvalg  17136  setsdm  17140  setsfun0  17142  setsid  17177  prdsval  17418  imasval  17474  mreexd  17603  mreexexlemd  17605  estrreslem2  18099  ipoval  18489  istsr  18542  mndpsuppss  18692  gsumzaddlem  19851  pwssplit1  20966  psrval  21824  psdmullem  22052  ordtval  23076  ordtcnv  23088  paste  23181  connsuba  23307  ptval2  23488  dfac14  23505  xkoptsub  23541  ptuncnv  23694  ptunhmeo  23695  xpstopnlem1  23696  alexsubALTlem3  23936  ustuqtop1  24129  rrxmvallem  25304  ovolioo  25469  uniiccdif  25479  itgsplitioo  25739  limcfval  25773  lhop2  25920  lgsquadlem2  27292  nodenselem5  27600  nosupbnd2lem1  27627  nosupbnd2  27628  noinfbnd2lem1  27642  noinfbnd2  27643  noetainflem2  27650  madeoldsuc  27796  lrold  27808  lrrecval  27846  addsval  27869  addsrid  27871  addscom  27873  addsproplem1  27876  addsprop  27883  addsass  27912  mulsval  28012  mulsrid  28016  mulsproplemcbv  28018  mulsproplem1  28019  mulsprop  28033  mulscom  28042  addsdi  28058  mulsass  28069  mulsunif2lem  28072  precsexlemcbv  28108  precsexlem3  28111  n0scut  28226  halfcut  28333  readdscl  28350  remulscl  28353  axlowdimlem13  28881  axlowdimlem15  28883  axlowdim  28888  eengv  28906  vtxdun  29409  trlsegvdeg  30156  numclwwlk3lem2lem  30312  ex-res  30370  imadifxp  32530  suppun2  32607  cnvprop  32619  mptprop  32621  coprprop  32622  fmptunsnop  32623  padct  32643  resf1o  32653  symgcom  33040  tocycfv  33066  tocycf  33074  tocyc01  33075  cycpm2tr  33076  cycpmco2f1  33081  cycpmco2rn  33082  cycpmconjv  33099  cycpmconjslem2  33112  elrgspnlem4  33196  rlocval  33210  idlsrgval  33474  rprmval  33487  zarclsun  33860  ordtprsval  33908  ordtprsuni  33909  ordtcnvNEW  33910  unelcarsg  34303  carsgclctunlem1  34308  eulerpartlemt  34362  sseqval  34379  probun  34410  bnj1373  35020  bnj1489  35046  cvmliftlem10  35281  satfvsuc  35348  satfdm  35356  satf0suc  35363  sat1el2xp  35366  fmlasuc0  35371  satffunlem1lem1  35389  satffunlem2lem1  35391  mrexval  35488  mrsubffval  35494  msrval  35525  mthmpps  35569  lineunray  36135  rdgssun  37366  exrecfnlem  37367  finixpnum  37599  ptrest  37613  poimirlem1  37615  poimirlem2  37616  poimirlem3  37617  poimirlem4  37618  poimirlem5  37619  poimirlem6  37620  poimirlem7  37621  poimirlem8  37622  poimirlem9  37623  poimirlem10  37624  poimirlem11  37625  poimirlem12  37626  poimirlem15  37629  poimirlem16  37630  poimirlem17  37631  poimirlem18  37632  poimirlem19  37633  poimirlem20  37634  poimirlem21  37635  poimirlem22  37636  poimirlem23  37637  poimirlem24  37638  poimirlem26  37640  poimirlem27  37641  poimirlem28  37642  poimirlem32  37646  mblfinlem2  37652  itg2addnclem2  37666  ldualset  39118  paddval  39792  paddcom  39807  dvafset  40998  dvaset  40999  dvhfset  41074  dvhset  41075  hdmapfval  41821  hlhilset  41928  dvun  42347  fsuppssindlem2  42580  istopclsd  42688  fzsplit1nn0  42742  diophrw  42747  eldioph2lem1  42748  eldioph2lem2  42749  diophin  42760  diophren  42801  pwssplit4  43078  mendval  43168  iocunico  43200  tfsconcatun  43326  tfsconcat0i  43334  onsucunitp  43362  oaun3  43371  rclexi  43604  rtrclex  43606  rtrclexi  43610  cnvrcl0  43614  dfrtrcl5  43618  dfrcl2  43663  dfrcl3  43664  iunrelexp0  43691  trclfvdecomr  43717  dfrtrcl4  43727  frege131d  43753  clsk3nimkb  44029  clsk1indlem3  44032  clsk1independent  44035  ntrclskb  44058  ntrclsk3  44059  ntrclsk13  44060  permaxinf2lem  45002  dvmptfprodlem  45942  caratheodorylem1  46524  ovnsubadd2lem  46643  ovolval4lem1  46647  fzopredsuc  47324  clnbgrval  47823  cycl3grtri  47946  aacllem  49790