Theorem uneq12d 4125

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

Syntax hints:   → wi 4   = wceq 1563   ∪ cun 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3912

This theorem is referenced by:  symdifeq1  4210  csbun  4398  csbprg  4671  disjpr2  4675  diftpsn3  4765  iunxprg  5057  relresdm1  6025  rnpropg  6212  suceqd  6417  fntpg  6585  foun  6829  f1oprswap  6856  fnimapr  6954  fnimatpd  6955  xpprsng  7126  residpr  7129  fvsnun2  7171  fsnunfv  7175  fsnunres  7176  f1ounsn  7260  f1ofvswap  7294  xpord2pred  8129  xpord3pred  8136  frrlem12  8282  oarec  8535  ereq1  8690  mapunen  9122  cnfcomlem  9656  trcl  9685  djueq12  9878  r0weon  9984  infxpen  9986  cfsmolem  10242  cfsmo  10243  axdc3lem4  10425  ttukeylem3  10483  ttukey2g  10488  alephadd  10550  fpwwe2lem12  10615  wunex2  10711  wuncval2  10720  inar1  10748  prunioo  13496  fztp  13596  fzsuc2  13598  fseq1p1m1  13614  s3tpop  14934  s4dom  14944  s2rn  14988  s3rn  14989  s7rn  14990  trclun  15039  relexp0g  15047  relexpsucnnr  15050  dfrtrcl2  15087  setsvalg  17214  setsdm  17218  setsfun0  17220  setsid  17255  prdsval  17496  imasval  17553  mreexd  17686  mreexexlemd  17688  estrreslem2  18182  ipoval  18574  istsr  18627  mndpsuppss  18811  gsumzaddlem  19979  pwssplit1  21146  psrval  22022  psdmullem  22285  ordtval  23303  ordtcnv  23315  paste  23408  connsuba  23534  ptval2  23715  dfac14  23732  xkoptsub  23768  ptuncnv  23921  ptunhmeo  23922  xpstopnlem1  23923  alexsubALTlem3  24163  ustuqtop1  24355  rrxmvallem  25520  ovolioo  25684  uniiccdif  25694  itgsplitioo  25954  limcfval  25988  lhop2  26131  lgsquadlem2  27499  nodenselem5  27806  nosupbnd2lem1  27833  nosupbnd2  27834  noinfbnd2lem1  27848  noinfbnd2  27849  noetainflem2  27856  madeoldsuc  28032  lrold  28044  lrrecval  28086  addsval  28109  addsrid  28111  addscom  28113  addsproplem1  28116  addsprop  28123  addsass  28152  mulsval  28256  mulsrid  28260  mulsproplemcbv  28262  mulsproplem1  28263  mulsprop  28277  mulscom  28286  addsdi  28302  mulsass  28313  mulsunif2lem  28316  precsexlemcbv  28353  precsexlem3  28356  n0cut  28481  halfcut  28605  pw2cut2  28609  readdscl  28646  remulscl  28649  axlowdimlem13  29209  axlowdimlem15  29211  axlowdim  29216  eengv  29234  vtxdun  29736  trlsegvdeg  30483  numclwwlk3lem2lem  30639  ex-res  30697  imadifxp  32852  fresunsn  32878  suppun2  32937  cnvprop  32949  mptprop  32951  coprprop  32952  fmptunsnop  32953  padct  32971  resf1o  32983  symgcom  33311  tocycfv  33337  tocycf  33345  tocyc01  33346  cycpm2tr  33347  cycpmco2f1  33352  cycpmco2rn  33353  cycpmconjv  33370  cycpmconjslem2  33383  elrgspnlem4  33473  rlocval  33487  idlsrgval  33705  rprmval  33718  extvfvcl  33838  zarclsun  34172  ordtprsval  34220  ordtprsuni  34221  ordtcnvNEW  34222  unelcarsg  34614  carsgclctunlem1  34619  eulerpartlemt  34673  sseqval  34690  probun  34721  bnj1373  35330  bnj1489  35356  cvmliftlem10  35652  satfvsuc  35719  satfdm  35727  satf0suc  35734  sat1el2xp  35737  fmlasuc0  35742  satffunlem1lem1  35760  satffunlem2lem1  35762  mrexval  35859  mrsubffval  35865  msrval  35896  mthmpps  35940  lineunray  36505  rdgssun  37879  exrecfnlem  37880  finixpnum  38111  ptrest  38125  poimirlem1  38127  poimirlem2  38128  poimirlem3  38129  poimirlem4  38130  poimirlem5  38131  poimirlem6  38132  poimirlem7  38133  poimirlem8  38134  poimirlem9  38135  poimirlem10  38136  poimirlem11  38137  poimirlem12  38138  poimirlem15  38141  poimirlem16  38142  poimirlem17  38143  poimirlem18  38144  poimirlem19  38145  poimirlem20  38146  poimirlem21  38147  poimirlem22  38148  poimirlem23  38149  poimirlem24  38150  poimirlem26  38152  poimirlem27  38153  poimirlem28  38154  poimirlem32  38158  mblfinlem2  38164  itg2addnclem2  38178  ecun  38899  ecuncnvepres  38901  ldualset  39756  paddval  40429  paddcom  40444  dvafset  41635  dvaset  41636  dvhfset  41711  dvhset  41712  hdmapfval  42458  hlhilset  42565  dvun  42975  fsuppssindlem2  43181  istopclsd  43288  fzsplit1nn0  43342  diophrw  43347  eldioph2lem1  43348  eldioph2lem2  43349  diophin  43360  diophren  43397  pwssplit4  43673  mendval  43763  iocunico  43795  tfsconcatun  43921  tfsconcat0i  43929  onsucunitp  43957  oaun3  43966  rclexi  44198  rtrclex  44200  rtrclexi  44204  cnvrcl0  44208  dfrtrcl5  44212  dfrcl2  44257  dfrcl3  44258  iunrelexp0  44285  trclfvdecomr  44311  dfrtrcl4  44321  frege131d  44347  clsk3nimkb  44623  clsk1indlem3  44626  clsk1independent  44629  ntrclskb  44652  ntrclsk3  44653  ntrclsk13  44654  permaxinf2lem  45580  dvmptfprodlem  46517  caratheodorylem1  47099  ovnsubadd2lem  47218  ovolval4lem1  47222  fzopredsuc  47917  clnbgrval  48443  cycl3grtri  48568  aacllem  50431