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

Theorem uneq12d 3801
 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 3795 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶) = (𝐵𝐷))
41, 2, 3syl2anc 694 1 (𝜑 → (𝐴𝐶) = (𝐵𝐷))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1523   ∪ cun 3605 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-un 3612 This theorem is referenced by:  symdifeq1  3879  csbun  4042  csbprg  4276  disjpr2  4280  disjpr2OLD  4281  diftpsn3  4364  diftpsn3OLD  4365  iunxprg  4639  rnpropg  5651  suceq  5828  fntpg  5986  foun  6193  f1oprswap  6218  fnimapr  6301  residpr  6449  fsnunfv  6494  fsnunres  6495  oarec  7687  ereq1  7794  mapunen  8170  cnfcomlem  8634  trcl  8642  r0weon  8873  infxpen  8875  cfsmolem  9130  cfsmo  9131  axdc3lem4  9313  ttukeylem3  9371  ttukey2g  9376  alephadd  9437  fpwwe2lem13  9502  wunex2  9598  wuncval2  9607  inar1  9635  prunioo  12339  fztp  12435  fzsuc2  12436  fseq1p1m1  12452  s3tpop  13700  s4dom  13710  trclun  13799  relexp0g  13806  relexpsucnnr  13809  dfrtrcl2  13846  setsvalg  15934  setsdm  15939  setsfun0  15941  setsid  15961  prdsval  16162  imasval  16218  mreexd  16349  mreexexlemd  16351  estrreslem2  16825  ipoval  17201  istsr  17264  gsumzaddlem  18367  pwssplit1  19107  psrval  19410  ordtval  21041  ordtcnv  21053  paste  21146  connsuba  21271  ptval2  21452  dfac14  21469  xkoptsub  21505  ptuncnv  21658  ptunhmeo  21659  xpstopnlem1  21660  alexsubALTlem3  21900  ustuqtop1  22092  rrxmvallem  23233  ovolioo  23382  uniiccdif  23392  itgsplitioo  23649  limcfval  23681  lhop2  23823  lgsquadlem2  25151  axlowdimlem13  25879  axlowdimlem15  25881  axlowdim  25886  eengv  25904  vtxdun  26433  trlsegvdeg  27205  numclwwlk3lemlem  27370  ex-res  27428  imadifxp  29540  funresdm1  29542  padct  29625  resf1o  29633  ordtprsval  30092  ordtprsuni  30093  ordtcnvNEW  30094  unelcarsg  30502  carsgclctunlem1  30507  eulerpartlemt  30561  sseqval  30578  probun  30609  bnj1373  31224  bnj1489  31250  cvmliftlem10  31402  mrexval  31524  mrsubffval  31530  msrval  31561  mthmpps  31605  nodenselem5  31963  nosupbnd2lem1  31986  nosupbnd2  31987  lineunray  32379  finixpnum  33524  ptrest  33538  poimirlem1  33540  poimirlem2  33541  poimirlem3  33542  poimirlem4  33543  poimirlem5  33544  poimirlem6  33545  poimirlem7  33546  poimirlem8  33547  poimirlem9  33548  poimirlem10  33549  poimirlem11  33550  poimirlem12  33551  poimirlem15  33554  poimirlem16  33555  poimirlem17  33556  poimirlem18  33557  poimirlem19  33558  poimirlem20  33559  poimirlem21  33560  poimirlem22  33561  poimirlem23  33562  poimirlem24  33563  poimirlem26  33565  poimirlem27  33566  poimirlem28  33567  poimirlem32  33571  mblfinlem2  33577  itg2addnclem2  33592  ldualset  34730  paddval  35402  paddcom  35417  dvafset  36609  dvaset  36610  dvhfset  36686  dvhset  36687  hdmapfval  37436  hlhilset  37543  istopclsd  37580  fzsplit1nn0  37634  diophrw  37639  eldioph2lem1  37640  eldioph2lem2  37641  diophin  37653  diophren  37694  pwssplit4  37976  mendval  38070  iocunico  38113  rclexi  38239  rtrclex  38241  rtrclexi  38245  cnvrcl0  38249  dfrtrcl5  38253  dfrcl2  38283  dfrcl3  38284  iunrelexp0  38311  trclfvdecomr  38337  dfrtrcl4  38347  frege131d  38373  clsk3nimkb  38655  clsk1indlem3  38658  clsk1independent  38661  ntrclskb  38684  ntrclsk3  38685  ntrclsk13  38686  dvmptfprodlem  40477  caratheodorylem1  41061  ovnsubadd2lem  41180  ovolval4lem1  41184  fzopredsuc  41658  xpprsng  42435  mndpsuppss  42477  aacllem  42875
 Copyright terms: Public domain W3C validator