Theorem uneq12d 4124

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

Syntax hints:   → wi 4   = wceq 1570   ∪ cun 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911

This theorem is referenced by:  symdifeq1  4209  csbun  4407  csbprg  4676  disjpr2  4680  diftpsn3  4771  iunxprg  5063  relresdm1  6037  rnpropg  6225  suceqd  6430  fntpg  6598  foun  6841  f1oprswap  6868  fnimapr  6966  fnimatpd  6967  xpprsng  7138  residpr  7141  fvsnun2  7183  fsnunfv  7187  fsnunres  7188  f1ounsn  7272  f1ofvswap  7306  xpord2pred  8142  xpord3pred  8149  frrlem12  8295  oarec  8548  ereq1  8703  mapunen  9135  cnfcomlem  9669  trcl  9698  djueq12  9891  r0weon  9997  infxpen  9999  cfsmolem  10255  cfsmo  10256  axdc3lem4  10438  ttukeylem3  10496  ttukey2g  10501  alephadd  10563  fpwwe2lem12  10628  wunex2  10724  wuncval2  10733  inar1  10761  prunioo  13509  fztp  13610  fzsuc2  13612  fseq1p1m1  13628  s3tpop  14948  s4dom  14958  s2rn  15002  s3rn  15003  s7rn  15004  trclun  15053  relexp0g  15061  relexpsucnnr  15064  dfrtrcl2  15101  setsvalg  17227  setsdm  17231  setsfun0  17233  setsid  17268  prdsval  17509  imasval  17566  mreexd  17699  mreexexlemd  17701  estrreslem2  18195  ipoval  18587  istsr  18640  mndpsuppss  18824  gsumzaddlem  19992  pwssplit1  21161  psrval  22046  psdmullem  22309  ordtval  23327  ordtcnv  23339  paste  23432  connsuba  23558  ptval2  23739  dfac14  23756  xkoptsub  23792  ptuncnv  23945  ptunhmeo  23946  xpstopnlem1  23947  alexsubALTlem3  24187  ustuqtop1  24379  rrxmvallem  25544  ovolioo  25708  uniiccdif  25718  itgsplitioo  25978  limcfval  26012  lhop2  26155  lgsquadlem2  27526  nodenselem5  27833  nosupbnd2lem1  27860  nosupbnd2  27861  noinfbnd2lem1  27875  noinfbnd2  27876  noetainflem2  27883  madeoldsuc  28059  lrold  28071  lrrecval  28113  addsval  28136  addsrid  28138  addscom  28140  addsproplem1  28143  addsprop  28150  addsass  28179  mulsval  28283  mulsrid  28287  mulsproplemcbv  28289  mulsproplem1  28290  mulsprop  28304  mulscom  28313  addsdi  28329  mulsass  28340  mulsunif2lem  28343  precsexlemcbv  28380  precsexlem3  28383  n0cut  28508  halfcut  28632  pw2cut2  28636  readdscl  28673  remulscl  28676  axlowdimlem13  29285  axlowdimlem15  29287  axlowdim  29292  eengv  29310  vtxdun  29812  trlsegvdeg  30559  numclwwlk3lem2lem  30715  ex-res  30773  imadifxp  32927  fresunsn  32951  suppun2  33010  cnvprop  33022  mptprop  33024  coprprop  33025  fmptunsnop  33026  padct  33044  resf1o  33056  symgcom  33384  tocycfv  33410  tocycf  33418  tocyc01  33419  cycpm2tr  33420  cycpmco2f1  33425  cycpmco2rn  33426  cycpmconjv  33443  cycpmconjslem2  33456  elrgspnlem4  33546  rlocval  33560  idlsrgval  33774  rprmval  33787  extvfvcl  33907  zarclsun  34241  ordtprsval  34289  ordtprsuni  34290  ordtcnvNEW  34291  unelcarsg  34683  carsgclctunlem1  34688  eulerpartlemt  34742  sseqval  34759  probun  34790  bnj1373  35399  bnj1489  35425  cvmliftlem10  35767  satfvsuc  35834  satfdm  35842  satf0suc  35849  sat1el2xp  35852  fmlasuc0  35857  satffunlem1lem1  35875  satffunlem2lem1  35877  mrexval  35974  mrsubffval  35980  msrval  36011  mthmpps  36055  lineunray  36620  rdgssun  38005  exrecfnlem  38006  finixpnum  38237  ptrest  38251  poimirlem1  38253  poimirlem2  38254  poimirlem3  38255  poimirlem4  38256  poimirlem5  38257  poimirlem6  38258  poimirlem7  38259  poimirlem8  38260  poimirlem9  38261  poimirlem10  38262  poimirlem11  38263  poimirlem12  38264  poimirlem15  38267  poimirlem16  38268  poimirlem17  38269  poimirlem18  38270  poimirlem19  38271  poimirlem20  38272  poimirlem21  38273  poimirlem22  38274  poimirlem23  38275  poimirlem24  38276  poimirlem26  38278  poimirlem27  38279  poimirlem28  38280  poimirlem32  38284  mblfinlem2  38290  itg2addnclem2  38304  ecun  39023  ecuncnvepres  39025  ldualset  39880  paddval  40553  paddcom  40568  dvafset  41759  dvaset  41760  dvhfset  41835  dvhset  41836  hdmapfval  42582  hlhilset  42689  dvun  43101  fsuppssindlem2  43307  istopclsd  43414  fzsplit1nn0  43468  diophrw  43473  eldioph2lem1  43474  eldioph2lem2  43475  diophin  43486  diophren  43523  pwssplit4  43799  mendval  43889  iocunico  43921  tfsconcatun  44047  tfsconcat0i  44055  onsucunitp  44083  oaun3  44092  rclexi  44324  rtrclex  44326  rtrclexi  44330  cnvrcl0  44334  dfrtrcl5  44338  dfrcl2  44383  dfrcl3  44384  iunrelexp0  44411  trclfvdecomr  44437  dfrtrcl4  44447  frege131d  44473  clsk3nimkb  44749  clsk1indlem3  44752  clsk1independent  44755  ntrclskb  44778  ntrclsk3  44779  ntrclsk13  44780  permaxinf2lem  45704  dvmptfprodlem  46641  caratheodorylem1  47223  ovnsubadd2lem  47342  ovolval4lem1  47346  fzopredsuc  48044  clnbgrval  48570  cycl3grtri  48695  aacllem  50584