MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  uneq12d Structured version   Visualization version   GIF version

Theorem uneq12d 4126
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
StepHypRef Expression
1 uneq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 uneq12d.2 . 2 (𝜑𝐶 = 𝐷)
3 uneq12 4120 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶) = (𝐵𝐷))
41, 2, 3syl2anc 587 1 (𝜑 → (𝐴𝐶) = (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  cun 3917
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-un 3924
This theorem is referenced by:  symdifeq1  4206  csbun  4373  csbprg  4630  disjpr2  4634  diftpsn3  4719  iunxprg  5004  rnpropg  6066  suceq  6243  fntpg  6402  foun  6624  f1oprswap  6649  fnimapr  6738  xpprsng  6893  residpr  6896  fvsnun2  6936  fsnunfv  6940  fsnunres  6941  oarec  8184  ereq1  8292  mapunen  8683  cnfcomlem  9159  trcl  9167  djueq12  9330  r0weon  9436  infxpen  9438  cfsmolem  9690  cfsmo  9691  axdc3lem4  9873  ttukeylem3  9931  ttukey2g  9936  alephadd  9997  fpwwe2lem13  10062  wunex2  10158  wuncval2  10167  inar1  10195  prunioo  12868  fztp  12967  fzsuc2  12969  fseq1p1m1  12985  s3tpop  14271  s4dom  14281  trclun  14374  relexp0g  14381  relexpsucnnr  14384  dfrtrcl2  14421  setsvalg  16512  setsdm  16517  setsfun0  16519  setsid  16538  prdsval  16728  imasval  16784  mreexd  16913  mreexexlemd  16915  estrreslem2  17388  ipoval  17764  istsr  17827  gsumzaddlem  19041  pwssplit1  19831  psrval  20607  ordtval  21800  ordtcnv  21812  paste  21905  connsuba  22031  ptval2  22212  dfac14  22229  xkoptsub  22265  ptuncnv  22418  ptunhmeo  22419  xpstopnlem1  22420  alexsubALTlem3  22660  ustuqtop1  22853  rrxmvallem  24014  ovolioo  24178  uniiccdif  24188  itgsplitioo  24447  limcfval  24481  lhop2  24624  lgsquadlem2  25971  axlowdimlem13  26754  axlowdimlem15  26756  axlowdim  26761  eengv  26779  vtxdun  27277  trlsegvdeg  28018  numclwwlk3lem2lem  28174  ex-res  28232  imadifxp  30365  funresdm1  30369  fnimatp  30437  cnvprop  30446  mptprop  30448  coprprop  30449  padct  30469  resf1o  30480  symgcom  30762  tocycfv  30786  tocycf  30794  tocyc01  30795  cycpm2tr  30796  cycpmco2f1  30801  cycpmco2rn  30802  cycpmconjv  30819  cycpmconjslem2  30832  idlsrgval  31029  ordtprsval  31221  ordtprsuni  31222  ordtcnvNEW  31223  unelcarsg  31630  carsgclctunlem1  31635  eulerpartlemt  31689  sseqval  31706  probun  31737  bnj1373  32362  bnj1489  32388  cvmliftlem10  32601  satfvsuc  32668  satfdm  32676  satf0suc  32683  sat1el2xp  32686  fmlasuc0  32691  satffunlem1lem1  32709  satffunlem2lem1  32711  mrexval  32808  mrsubffval  32814  msrval  32845  mthmpps  32889  frrlem12  33194  nodenselem5  33252  nosupbnd2lem1  33275  nosupbnd2  33276  lineunray  33668  rdgssun  34743  exrecfnlem  34744  finixpnum  34990  ptrest  35004  poimirlem1  35006  poimirlem2  35007  poimirlem3  35008  poimirlem4  35009  poimirlem5  35010  poimirlem6  35011  poimirlem7  35012  poimirlem8  35013  poimirlem9  35014  poimirlem10  35015  poimirlem11  35016  poimirlem12  35017  poimirlem15  35020  poimirlem16  35021  poimirlem17  35022  poimirlem18  35023  poimirlem19  35024  poimirlem20  35025  poimirlem21  35026  poimirlem22  35027  poimirlem23  35028  poimirlem24  35029  poimirlem26  35031  poimirlem27  35032  poimirlem28  35033  poimirlem32  35037  mblfinlem2  35043  itg2addnclem2  35057  ldualset  36369  paddval  37042  paddcom  37057  dvafset  38248  dvaset  38249  dvhfset  38324  dvhset  38325  hdmapfval  39071  hlhilset  39178  metakunt17  39315  metakunt20  39318  metakunt21  39319  metakunt22  39320  metakunt24  39322  istopclsd  39561  fzsplit1nn0  39615  diophrw  39620  eldioph2lem1  39621  eldioph2lem2  39622  diophin  39633  diophren  39674  pwssplit4  39953  mendval  40047  iocunico  40081  rclexi  40235  rtrclex  40237  rtrclexi  40241  cnvrcl0  40245  dfrtrcl5  40249  dfrcl2  40295  dfrcl3  40296  iunrelexp0  40323  trclfvdecomr  40349  dfrtrcl4  40359  frege131d  40385  clsk3nimkb  40666  clsk1indlem3  40669  clsk1independent  40672  ntrclskb  40695  ntrclsk3  40696  ntrclsk13  40697  dvmptfprodlem  42516  caratheodorylem1  43095  ovnsubadd2lem  43214  ovolval4lem1  43218  fzopredsuc  43810  mndpsuppss  44703  aacllem  45259
  Copyright terms: Public domain W3C validator