Theorem uneq12d 4169

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956

This theorem is referenced by:  symdifeq1  4255  csbun  4441  csbprg  4709  disjpr2  4713  diftpsn3  4802  iunxprg  5096  relresdm1  6051  rnpropg  6242  suceq  6450  fntpg  6626  foun  6866  f1oprswap  6892  fnimapr  6992  fnimatpd  6993  xpprsng  7160  residpr  7163  fvsnun2  7203  fsnunfv  7207  fsnunres  7208  f1ounsn  7292  f1ofvswap  7326  xpord2pred  8170  xpord3pred  8177  frrlem12  8322  oarec  8600  ereq1  8752  mapunen  9186  cnfcomlem  9739  trcl  9768  djueq12  9944  r0weon  10052  infxpen  10054  cfsmolem  10310  cfsmo  10311  axdc3lem4  10493  ttukeylem3  10551  ttukey2g  10556  alephadd  10617  fpwwe2lem12  10682  wunex2  10778  wuncval2  10787  inar1  10815  prunioo  13521  fztp  13620  fzsuc2  13622  fseq1p1m1  13638  s3tpop  14948  s4dom  14958  s2rn  15002  s3rn  15003  s7rn  15004  trclun  15053  relexp0g  15061  relexpsucnnr  15064  dfrtrcl2  15101  setsvalg  17203  setsdm  17207  setsfun0  17209  setsid  17244  prdsval  17500  imasval  17556  mreexd  17685  mreexexlemd  17687  estrreslem2  18183  ipoval  18575  istsr  18628  mndpsuppss  18778  gsumzaddlem  19939  pwssplit1  21058  psrval  21935  psdmullem  22169  ordtval  23197  ordtcnv  23209  paste  23302  connsuba  23428  ptval2  23609  dfac14  23626  xkoptsub  23662  ptuncnv  23815  ptunhmeo  23816  xpstopnlem1  23817  alexsubALTlem3  24057  ustuqtop1  24250  rrxmvallem  25438  ovolioo  25603  uniiccdif  25613  itgsplitioo  25873  limcfval  25907  lhop2  26054  lgsquadlem2  27425  nodenselem5  27733  nosupbnd2lem1  27760  nosupbnd2  27761  noinfbnd2lem1  27775  noinfbnd2  27776  noetainflem2  27783  madeoldsuc  27923  lrold  27935  lrrecval  27972  addsval  27995  addsrid  27997  addscom  27999  addsproplem1  28002  addsprop  28009  addsass  28038  mulsval  28135  mulsrid  28139  mulsproplemcbv  28141  mulsproplem1  28142  mulsprop  28156  mulscom  28165  addsdi  28181  mulsass  28192  mulsunif2lem  28195  precsexlemcbv  28230  precsexlem3  28233  n0scut  28338  halfcut  28416  pw2bday  28418  readdscl  28431  remulscl  28434  axlowdimlem13  28969  axlowdimlem15  28971  axlowdim  28976  eengv  28994  vtxdun  29499  trlsegvdeg  30246  numclwwlk3lem2lem  30402  ex-res  30460  imadifxp  32614  suppun2  32693  cnvprop  32705  mptprop  32707  coprprop  32708  fmptunsnop  32709  padct  32731  resf1o  32741  symgcom  33103  tocycfv  33129  tocycf  33137  tocyc01  33138  cycpm2tr  33139  cycpmco2f1  33144  cycpmco2rn  33145  cycpmconjv  33162  cycpmconjslem2  33175  elrgspnlem4  33249  rlocval  33263  idlsrgval  33531  rprmval  33544  zarclsun  33869  ordtprsval  33917  ordtprsuni  33918  ordtcnvNEW  33919  unelcarsg  34314  carsgclctunlem1  34319  eulerpartlemt  34373  sseqval  34390  probun  34421  bnj1373  35044  bnj1489  35070  cvmliftlem10  35299  satfvsuc  35366  satfdm  35374  satf0suc  35381  sat1el2xp  35384  fmlasuc0  35389  satffunlem1lem1  35407  satffunlem2lem1  35409  mrexval  35506  mrsubffval  35512  msrval  35543  mthmpps  35587  lineunray  36148  rdgssun  37379  exrecfnlem  37380  finixpnum  37612  ptrest  37626  poimirlem1  37628  poimirlem2  37629  poimirlem3  37630  poimirlem4  37631  poimirlem5  37632  poimirlem6  37633  poimirlem7  37634  poimirlem8  37635  poimirlem9  37636  poimirlem10  37637  poimirlem11  37638  poimirlem12  37639  poimirlem15  37642  poimirlem16  37643  poimirlem17  37644  poimirlem18  37645  poimirlem19  37646  poimirlem20  37647  poimirlem21  37648  poimirlem22  37649  poimirlem23  37650  poimirlem24  37651  poimirlem26  37653  poimirlem27  37654  poimirlem28  37655  poimirlem32  37659  mblfinlem2  37665  itg2addnclem2  37679  ldualset  39126  paddval  39800  paddcom  39815  dvafset  41006  dvaset  41007  dvhfset  41082  dvhset  41083  hdmapfval  41829  hlhilset  41936  metakunt17  42222  metakunt20  42225  metakunt21  42226  metakunt22  42227  metakunt24  42229  dvun  42389  fsuppssindlem2  42602  istopclsd  42711  fzsplit1nn0  42765  diophrw  42770  eldioph2lem1  42771  eldioph2lem2  42772  diophin  42783  diophren  42824  pwssplit4  43101  mendval  43191  iocunico  43223  tfsconcatun  43350  tfsconcat0i  43358  onsucunitp  43386  oaun3  43395  rclexi  43628  rtrclex  43630  rtrclexi  43634  cnvrcl0  43638  dfrtrcl5  43642  dfrcl2  43687  dfrcl3  43688  iunrelexp0  43715  trclfvdecomr  43741  dfrtrcl4  43751  frege131d  43777  clsk3nimkb  44053  clsk1indlem3  44056  clsk1independent  44059  ntrclskb  44082  ntrclsk3  44083  ntrclsk13  44084  dvmptfprodlem  45959  caratheodorylem1  46541  ovnsubadd2lem  46660  ovolval4lem1  46664  fzopredsuc  47335  clnbgrval  47809  cycl3grtri  47914  aacllem  49320