Theorem uneq12d 4122

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

Syntax hints:   → wi 4   = wceq 1559   ∪ cun 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3909

This theorem is referenced by:  symdifeq1  4207  csbun  4394  csbprg  4667  disjpr2  4671  diftpsn3  4761  iunxprg  5052  relresdm1  6019  rnpropg  6205  suceqd  6409  fntpg  6577  foun  6821  f1oprswap  6848  fnimapr  6946  fnimatpd  6947  xpprsng  7118  residpr  7121  fvsnun2  7163  fsnunfv  7167  fsnunres  7168  f1ounsn  7252  f1ofvswap  7286  xpord2pred  8120  xpord3pred  8127  frrlem12  8273  oarec  8526  ereq1  8681  mapunen  9114  cnfcomlem  9651  trcl  9680  djueq12  9859  r0weon  9965  infxpen  9967  cfsmolem  10224  cfsmo  10225  axdc3lem4  10407  ttukeylem3  10465  ttukey2g  10470  alephadd  10532  fpwwe2lem12  10597  wunex2  10693  wuncval2  10702  inar1  10730  prunioo  13482  fztp  13582  fzsuc2  13584  fseq1p1m1  13600  s3tpop  14919  s4dom  14929  s2rn  14973  s3rn  14974  s7rn  14975  trclun  15024  relexp0g  15032  relexpsucnnr  15035  dfrtrcl2  15072  setsvalg  17185  setsdm  17189  setsfun0  17191  setsid  17226  prdsval  17467  imasval  17524  mreexd  17657  mreexexlemd  17659  estrreslem2  18153  ipoval  18545  istsr  18598  mndpsuppss  18782  gsumzaddlem  19944  pwssplit1  21106  psrval  21947  psdmullem  22210  ordtval  23229  ordtcnv  23241  paste  23334  connsuba  23460  ptval2  23641  dfac14  23658  xkoptsub  23694  ptuncnv  23847  ptunhmeo  23848  xpstopnlem1  23849  alexsubALTlem3  24089  ustuqtop1  24281  rrxmvallem  25446  ovolioo  25610  uniiccdif  25620  itgsplitioo  25880  limcfval  25914  lhop2  26057  lgsquadlem2  27422  nodenselem5  27729  nosupbnd2lem1  27756  nosupbnd2  27757  noinfbnd2lem1  27771  noinfbnd2  27772  noetainflem2  27779  madeoldsuc  27955  lrold  27967  lrrecval  28009  addsval  28032  addsrid  28034  addscom  28036  addsproplem1  28039  addsprop  28046  addsass  28075  mulsval  28179  mulsrid  28183  mulsproplemcbv  28185  mulsproplem1  28186  mulsprop  28200  mulscom  28209  addsdi  28225  mulsass  28236  mulsunif2lem  28239  precsexlemcbv  28276  precsexlem3  28279  n0cut  28404  halfcut  28528  pw2cut2  28532  readdscl  28569  remulscl  28572  axlowdimlem13  29101  axlowdimlem15  29103  axlowdim  29108  eengv  29126  vtxdun  29628  trlsegvdeg  30375  numclwwlk3lem2lem  30531  ex-res  30589  imadifxp  32750  fresunsn  32777  suppun2  32836  cnvprop  32848  mptprop  32850  coprprop  32851  fmptunsnop  32852  padct  32870  resf1o  32882  symgcom  33224  tocycfv  33250  tocycf  33258  tocyc01  33259  cycpm2tr  33260  cycpmco2f1  33265  cycpmco2rn  33266  cycpmconjv  33283  cycpmconjslem2  33296  elrgspnlem4  33387  rlocval  33401  idlsrgval  33660  rprmval  33673  extvfvcl  33794  zarclsun  34128  ordtprsval  34176  ordtprsuni  34177  ordtcnvNEW  34178  unelcarsg  34570  carsgclctunlem1  34575  eulerpartlemt  34629  sseqval  34646  probun  34677  bnj1373  35289  bnj1489  35315  cvmliftlem10  35608  satfvsuc  35675  satfdm  35683  satf0suc  35690  sat1el2xp  35693  fmlasuc0  35698  satffunlem1lem1  35716  satffunlem2lem1  35718  mrexval  35815  mrsubffval  35821  msrval  35852  mthmpps  35896  lineunray  36461  rdgssun  37836  exrecfnlem  37837  finixpnum  38068  ptrest  38082  poimirlem1  38084  poimirlem2  38085  poimirlem3  38086  poimirlem4  38087  poimirlem5  38088  poimirlem6  38089  poimirlem7  38090  poimirlem8  38091  poimirlem9  38092  poimirlem10  38093  poimirlem11  38094  poimirlem12  38095  poimirlem15  38098  poimirlem16  38099  poimirlem17  38100  poimirlem18  38101  poimirlem19  38102  poimirlem20  38103  poimirlem21  38104  poimirlem22  38105  poimirlem23  38106  poimirlem24  38107  poimirlem26  38109  poimirlem27  38110  poimirlem28  38111  poimirlem32  38115  mblfinlem2  38121  itg2addnclem2  38135  ecun  38856  ecuncnvepres  38858  ldualset  39713  paddval  40386  paddcom  40401  dvafset  41592  dvaset  41593  dvhfset  41668  dvhset  41669  hdmapfval  42415  hlhilset  42522  dvun  42932  fsuppssindlem2  43138  istopclsd  43245  fzsplit1nn0  43299  diophrw  43304  eldioph2lem1  43305  eldioph2lem2  43306  diophin  43317  diophren  43354  pwssplit4  43630  mendval  43720  iocunico  43752  tfsconcatun  43878  tfsconcat0i  43886  onsucunitp  43914  oaun3  43923  rclexi  44155  rtrclex  44157  rtrclexi  44161  cnvrcl0  44165  dfrtrcl5  44169  dfrcl2  44214  dfrcl3  44215  iunrelexp0  44242  trclfvdecomr  44268  dfrtrcl4  44278  frege131d  44304  clsk3nimkb  44580  clsk1indlem3  44583  clsk1independent  44586  ntrclskb  44609  ntrclsk3  44610  ntrclsk13  44611  permaxinf2lem  45552  dvmptfprodlem  46482  caratheodorylem1  47064  ovnsubadd2lem  47183  ovolval4lem1  47187  fzopredsuc  47882  clnbgrval  48408  cycl3grtri  48533  aacllem  50386