Theorem uneq12d 4178

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

Syntax hints:   → wi 4   = wceq 1536   ∪ cun 3960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-un 3967

This theorem is referenced by:  symdifeq1  4260  csbun  4446  csbprg  4713  disjpr2  4717  diftpsn3  4806  iunxprg  5100  relresdm1  6052  rnpropg  6243  suceq  6451  fntpg  6627  foun  6866  f1oprswap  6892  fnimapr  6991  fnimatpd  6992  xpprsng  7159  residpr  7162  fvsnun2  7202  fsnunfv  7206  fsnunres  7207  f1ounsn  7291  f1ofvswap  7325  xpord2pred  8168  xpord3pred  8175  frrlem12  8320  oarec  8598  ereq1  8750  mapunen  9184  cnfcomlem  9736  trcl  9765  djueq12  9941  r0weon  10049  infxpen  10051  cfsmolem  10307  cfsmo  10308  axdc3lem4  10490  ttukeylem3  10548  ttukey2g  10553  alephadd  10614  fpwwe2lem12  10679  wunex2  10775  wuncval2  10784  inar1  10812  prunioo  13517  fztp  13616  fzsuc2  13618  fseq1p1m1  13634  s3tpop  14944  s4dom  14954  s2rn  14998  s3rn  14999  s7rn  15000  trclun  15049  relexp0g  15057  relexpsucnnr  15060  dfrtrcl2  15097  setsvalg  17199  setsdm  17203  setsfun0  17205  setsid  17241  prdsval  17501  imasval  17557  mreexd  17686  mreexexlemd  17688  estrreslem2  18193  ipoval  18587  istsr  18640  mndpsuppss  18790  gsumzaddlem  19953  pwssplit1  21075  psrval  21952  psdmullem  22186  ordtval  23212  ordtcnv  23224  paste  23317  connsuba  23443  ptval2  23624  dfac14  23641  xkoptsub  23677  ptuncnv  23830  ptunhmeo  23831  xpstopnlem1  23832  alexsubALTlem3  24072  ustuqtop1  24265  rrxmvallem  25451  ovolioo  25616  uniiccdif  25626  itgsplitioo  25887  limcfval  25921  lhop2  26068  lgsquadlem2  27439  nodenselem5  27747  nosupbnd2lem1  27774  nosupbnd2  27775  noinfbnd2lem1  27789  noinfbnd2  27790  noetainflem2  27797  madeoldsuc  27937  lrold  27949  lrrecval  27986  addsval  28009  addsrid  28011  addscom  28013  addsproplem1  28016  addsprop  28023  addsass  28052  mulsval  28149  mulsrid  28153  mulsproplemcbv  28155  mulsproplem1  28156  mulsprop  28170  mulscom  28179  addsdi  28195  mulsass  28206  mulsunif2lem  28209  precsexlemcbv  28244  precsexlem3  28247  n0scut  28352  halfcut  28430  pw2bday  28432  readdscl  28445  remulscl  28448  axlowdimlem13  28983  axlowdimlem15  28985  axlowdim  28990  eengv  29008  vtxdun  29513  trlsegvdeg  30255  numclwwlk3lem2lem  30411  ex-res  30469  imadifxp  32620  suppun2  32698  cnvprop  32710  mptprop  32712  coprprop  32713  fmptunsnop  32714  padct  32736  resf1o  32747  symgcom  33085  tocycfv  33111  tocycf  33119  tocyc01  33120  cycpm2tr  33121  cycpmco2f1  33126  cycpmco2rn  33127  cycpmconjv  33144  cycpmconjslem2  33157  elrgspnlem4  33234  rlocval  33245  idlsrgval  33510  rprmval  33523  zarclsun  33830  ordtprsval  33878  ordtprsuni  33879  ordtcnvNEW  33880  unelcarsg  34293  carsgclctunlem1  34298  eulerpartlemt  34352  sseqval  34369  probun  34400  bnj1373  35022  bnj1489  35048  cvmliftlem10  35278  satfvsuc  35345  satfdm  35353  satf0suc  35360  sat1el2xp  35363  fmlasuc0  35368  satffunlem1lem1  35386  satffunlem2lem1  35388  mrexval  35485  mrsubffval  35491  msrval  35522  mthmpps  35566  lineunray  36128  rdgssun  37360  exrecfnlem  37361  finixpnum  37591  ptrest  37605  poimirlem1  37607  poimirlem2  37608  poimirlem3  37609  poimirlem4  37610  poimirlem5  37611  poimirlem6  37612  poimirlem7  37613  poimirlem8  37614  poimirlem9  37615  poimirlem10  37616  poimirlem11  37617  poimirlem12  37618  poimirlem15  37621  poimirlem16  37622  poimirlem17  37623  poimirlem18  37624  poimirlem19  37625  poimirlem20  37626  poimirlem21  37627  poimirlem22  37628  poimirlem23  37629  poimirlem24  37630  poimirlem26  37632  poimirlem27  37633  poimirlem28  37634  poimirlem32  37638  mblfinlem2  37644  itg2addnclem2  37658  ldualset  39106  paddval  39780  paddcom  39795  dvafset  40986  dvaset  40987  dvhfset  41062  dvhset  41063  hdmapfval  41809  hlhilset  41916  metakunt17  42202  metakunt20  42205  metakunt21  42206  metakunt22  42207  metakunt24  42209  dvun  42367  fsuppssindlem2  42578  istopclsd  42687  fzsplit1nn0  42741  diophrw  42746  eldioph2lem1  42747  eldioph2lem2  42748  diophin  42759  diophren  42800  pwssplit4  43077  mendval  43167  iocunico  43199  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  dvmptfprodlem  45899  caratheodorylem1  46481  ovnsubadd2lem  46600  ovolval4lem1  46604  fzopredsuc  47272  clnbgrval  47746  aacllem  49031