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

Theorem uneq12d 3967
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 3961 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶) = (𝐵𝐷))
41, 2, 3syl2anc 575 1 (𝜑 → (𝐴𝐶) = (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  cun 3767
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-v 3393  df-un 3774
This theorem is referenced by:  symdifeq1  4044  csbun  4207  csbprg  4436  disjpr2  4440  diftpsn3  4523  iunxprg  4799  rnpropg  5827  suceq  6002  fntpg  6156  foun  6367  f1oprswap  6392  fnimapr  6479  residpr  6628  fsnunfv  6674  fsnunres  6675  oarec  7875  ereq1  7982  mapunen  8364  cnfcomlem  8839  trcl  8847  djueq12  9010  r0weon  9114  infxpen  9116  cfsmolem  9373  cfsmo  9374  axdc3lem4  9556  ttukeylem3  9614  ttukey2g  9619  alephadd  9680  fpwwe2lem13  9745  wunex2  9841  wuncval2  9850  inar1  9878  prunioo  12520  fztp  12616  fzsuc2  12617  fseq1p1m1  12633  s3tpop  13874  s4dom  13884  trclun  13974  relexp0g  13981  relexpsucnnr  13984  dfrtrcl2  14021  setsvalg  16094  setsdm  16099  setsfun0  16101  setsid  16121  prdsval  16316  imasval  16372  mreexd  16503  mreexexlemd  16505  estrreslem2  16978  ipoval  17355  istsr  17418  gsumzaddlem  18518  pwssplit1  19262  psrval  19567  ordtval  21204  ordtcnv  21216  paste  21309  connsuba  21434  ptval2  21615  dfac14  21632  xkoptsub  21668  ptuncnv  21821  ptunhmeo  21822  xpstopnlem1  21823  alexsubALTlem3  22063  ustuqtop1  22255  rrxmvallem  23398  ovolioo  23548  uniiccdif  23558  itgsplitioo  23817  limcfval  23849  lhop2  23991  lgsquadlem2  25319  axlowdimlem13  26047  axlowdimlem15  26049  axlowdim  26054  eengv  26072  vtxdun  26604  trlsegvdeg  27399  numclwwlk3lem2lem  27570  ex-res  27628  imadifxp  29738  funresdm1  29740  padct  29823  resf1o  29831  ordtprsval  30288  ordtprsuni  30289  ordtcnvNEW  30290  unelcarsg  30698  carsgclctunlem1  30703  eulerpartlemt  30757  sseqval  30774  probun  30805  bnj1373  31419  bnj1489  31445  cvmliftlem10  31597  mrexval  31719  mrsubffval  31725  msrval  31756  mthmpps  31800  nodenselem5  32157  nosupbnd2lem1  32180  nosupbnd2  32181  lineunray  32573  finixpnum  33705  ptrest  33719  poimirlem1  33721  poimirlem2  33722  poimirlem3  33723  poimirlem4  33724  poimirlem5  33725  poimirlem6  33726  poimirlem7  33727  poimirlem8  33728  poimirlem9  33729  poimirlem10  33730  poimirlem11  33731  poimirlem12  33732  poimirlem15  33735  poimirlem16  33736  poimirlem17  33737  poimirlem18  33738  poimirlem19  33739  poimirlem20  33740  poimirlem21  33741  poimirlem22  33742  poimirlem23  33743  poimirlem24  33744  poimirlem26  33746  poimirlem27  33747  poimirlem28  33748  poimirlem32  33752  mblfinlem2  33758  itg2addnclem2  33772  ldualset  34903  paddval  35576  paddcom  35591  dvafset  36782  dvaset  36783  dvhfset  36858  dvhset  36859  hdmapfval  37605  hlhilset  37712  istopclsd  37762  fzsplit1nn0  37816  diophrw  37821  eldioph2lem1  37822  eldioph2lem2  37823  diophin  37835  diophren  37876  pwssplit4  38157  mendval  38251  iocunico  38293  rclexi  38419  rtrclex  38421  rtrclexi  38425  cnvrcl0  38429  dfrtrcl5  38433  dfrcl2  38463  dfrcl3  38464  iunrelexp0  38491  trclfvdecomr  38517  dfrtrcl4  38527  frege131d  38553  clsk3nimkb  38835  clsk1indlem3  38838  clsk1independent  38841  ntrclskb  38864  ntrclsk3  38865  ntrclsk13  38866  dvmptfprodlem  40636  caratheodorylem1  41219  ovnsubadd2lem  41338  ovolval4lem1  41342  fzopredsuc  41905  xpprsng  42675  mndpsuppss  42717  aacllem  43115
  Copyright terms: Public domain W3C validator