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

Theorem eqssd 3970
Description: Equality deduction from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 27-Jun-2004.)
Hypotheses
Ref Expression
eqssd.1 (𝜑𝐴𝐵)
eqssd.2 (𝜑𝐵𝐴)
Assertion
Ref Expression
eqssd (𝜑𝐴 = 𝐵)

Proof of Theorem eqssd
StepHypRef Expression
1 eqssd.1 . 2 (𝜑𝐴𝐵)
2 eqssd.2 . 2 (𝜑𝐵𝐴)
3 eqss 3968 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
41, 2, 3sylanbrc 586 1 (𝜑𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wss 3919
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-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-in 3926  df-ss 3936
This theorem is referenced by:  eqelssd  3974  uneqdifeq  4421  pweq  4538  unieq  4835  unissel  4855  intmin  4882  unissint  4886  int0el  4893  dmcosseq  5833  sofld  6033  relfld  6115  preddowncl  6164  wfi  6170  tz7.7  6206  fimacnv  6832  knatar  7105  sorpssuni  7454  sorpssint  7455  onint  7506  fo2ndf  7815  suppimacnv  7839  tposeq  7892  onfununi  7976  tfrlem15  8026  oaass  8185  odi  8203  omass  8204  oelim2  8219  oeeui  8226  nnawordex  8261  oaabslem  8268  oaabs2  8270  omabslem  8271  omabs  8272  uniinqs  8375  sucdom2  8625  fineqv  8732  dffi2  8886  fiuni  8891  dffi3  8894  hartogslem1  9005  ixpiunwdom  9053  cantnfp1lem3  9142  oemapvali  9146  cantnf  9155  r1val1  9214  rankval3b  9254  rankunb  9278  rankuni2b  9281  rankr1id  9290  rankc2  9299  rankxplim  9307  tcrank  9312  carden2b  9395  harval2  9425  en2other2  9435  infpwfien  9488  coflim  9683  cfcof  9696  cfidm  9697  isf32lem2  9776  fin1a2lem11  9832  fin1a2lem13  9834  ttukeylem7  9937  fpwwe2  10065  winafp  10119  wuncidm  10168  wuncval2  10169  tskuni  10205  grur1  10242  distrpr  10450  ltexpri  10465  reclem4pr  10472  fzopth  12950  fzosplit  13076  fzouzsplit  13078  ccatrn  13945  cotrtrclfv  14374  dmtrclfv  14380  dfrtrcl2  14423  structcnvcnv  16499  imasaddfnlem  16803  imasvscafn  16812  mrcuni  16894  mressmrcd  16900  submrc  16901  ssceq  17098  rescabs  17105  setcepi  17350  clatl  17728  ipopos  17772  psdmrn  17819  dirdm  17846  gsumress  17894  gsumvallem2  18000  gsumwspan  18013  trivsubgd  18307  trivsubgsnd  18308  trivnsgd  18326  cycsubg  18353  conjnmz  18394  pmtrprfv  18583  symggen  18600  odf1o2  18700  gex1  18718  sylow2alem1  18744  smndlsmidm  18783  lsmidmOLD  18791  lsmss1  18793  lsmss2  18795  lsmmod  18803  lsmdisj  18809  lsmdisj2  18810  cntzcmn  18962  prmcyg  19016  dmdprdd  19123  dprdspan  19151  dprdres  19152  dprdz  19154  subgdmdprd  19158  subgdprd  19159  dprddisj2  19163  dprd2dlem1  19165  dprd2da  19166  dmdprdsplit2lem  19169  dprdsplit  19172  ablfacrp  19190  pgpfac1lem3  19201  kerf1ghm  19500  issubdrg  19562  lspun  19761  lspsn  19776  lspsnneg  19780  lsp0  19783  lsslsp  19789  lmhmlsp  19823  lspextmo  19830  lsmsp  19860  lspprabs  19869  lspsnvs  19888  lspdisj  19899  lsmcv  19915  lspsnat  19919  lsppratlem6  19926  lspprat  19927  lbsextlem4  19935  lidl1el  19993  drngnidl  20004  lidldvgen  20030  cnsubrg  20160  mulgrhm2  20201  znrrg  20266  ocvin  20372  ocvlsp  20374  mrccss  20392  topsn  21545  eltg4i  21574  unitg  21581  tgtop  21587  tgidm  21594  en2top  21599  basgen  21602  2basgen  21604  fctop  21618  cctop  21620  ppttop  21621  epttop  21623  ntrin  21675  isopn3  21680  opnnei  21734  neiuni  21736  maxlp  21761  clslp  21762  tgrest  21773  resttopon  21775  rest0  21783  restcls  21795  restntr  21796  ordtbas2  21805  ordtbas  21806  ordtrest2  21818  cmpcov2  22004  tgcmp  22015  cmpcld  22016  uncmp  22017  cmpfi  22022  dis2ndc  22074  restnlly  22096  dislly  22111  comppfsc  22146  kgentopon  22152  kgencmp  22159  kgenidm  22161  iskgen2  22162  kgencn3  22172  ptuni2  22190  ptbasfi  22195  xkouni  22213  txcls  22218  txdis  22246  txindis  22248  txcmplem2  22256  xkopt  22269  txconn  22303  qtopval2  22310  qtopuni  22316  qtoprest  22331  qtopomap  22332  qtopcmap  22333  kqsat  22345  kqcldsat  22347  hmeocls  22382  hmeontr  22383  hmphdis  22410  fgfil  22489  fgabs  22493  trfil1  22500  fgtr  22504  uzrest  22511  ufilmax  22521  ufileu  22533  filufint  22534  ufildom1  22540  rnelfm  22567  flimfil  22583  uffclsflim  22645  alexsublem  22658  alexsubALTlem3  22663  alexsubALT  22665  ptcmplem2  22667  ptcmplem3  22668  tgpconncompeqg  22726  haustsms2  22751  tgptsmscls  22764  ust0  22834  ustbas2  22840  iccntr  23435  pi1xfrcnv  23671  clsocv  23863  cfilfcls  23887  equivcmet  23930  hlhil  24056  evthicc2  24073  ovolshft  24124  volsup  24169  dyadmbllem  24212  mbfconstlem  24240  itg11  24304  limciun  24506  dvnres  24543  cpnord  24547  dvcmulf  24557  dvmptcmul  24576  dvcnvre  24631  plyco0  24798  taylthlem1  24977  taylthlem2  24978  ulmdvlem3  25006  wilthlem2  25663  ppisval  25698  ppinprm  25746  chtnprm  25748  upgrex  26894  uvtxnbgr  27199  cusgredg  27223  ubthlem1  28662  pjhth  29185  ococin  29200  chsupsn  29205  ssjo  29239  chabs1  29308  spansncvi  29444  mdslj1i  30111  mdslj2i  30112  atomli  30174  atcvatlem  30177  atcvat3i  30188  sumdmdlem  30210  difininv  30297  fnpreimac  30435  pmtrcnelor  30777  cycpmrn  30827  rspidlid  30982  dimkerim  31091  cmpcref  31183  zarcls1  31202  zarclssn  31206  zart0  31211  xpinpreima2  31235  ordtrest2NEW  31251  sigagenid  31495  imambfm  31605  reprinfz1  31978  bnj1136  32354  bnj1398  32391  bnj1408  32393  bnj1498  32418  sconnpi1  32571  cvmliftlem15  32630  dftrpred3g  33157  trpredpo  33159  frpoind  33165  frind  33170  frrlem14  33221  sltval2  33248  noextenddif  33260  scutun12  33356  altopthsn  33507  opnbnd  33758  opnregcld  33763  cldregopn  33764  fnessref  33790  neibastop1  33792  topmeet  33797  topjoin  33798  fnemeet1  33799  fnejoin1  33801  bj-restpw  34479  bj-restb  34481  bj-restuni2  34485  dissneqlem  34729  pibt2  34806  lindsenlbs  35024  poimirlem13  35042  poimirlem14  35043  poimirlem15  35044  fdc  35155  sstotbnd2  35184  isbnd2  35193  totbndbnd  35199  prdstotbnd  35204  heibor1  35220  1idl  35436  igenval2  35476  idreseqidinxp  35699  lshpdisj  36255  lssats  36280  lsatcvat3  36320  lshpset2N  36387  lfl1dim  36389  lfl1dim2N  36390  lkrpssN  36431  paddass  37106  paddidm  37109  pmod1i  37116  pmapjat1  37121  pclbtwnN  37165  pclunN  37166  paddunN  37195  pclfinclN  37218  dihjust  38485  dihmeetlem1N  38558  dihglblem5apreN  38559  dihmeetlem13N  38587  dochocsp  38647  dochdmj1  38658  dochnoncon  38659  dihjatb  38684  dihjat1lem  38696  lcfl9a  38773  lclkrlem2s  38793  lclkrlem2v  38796  mapdrvallem3  38914  mapdunirnN  38918  mapdin  38930  mapdlsm  38932  baerlem3lem2  38978  baerlem5alem2  38979  baerlem5blem2  38980  hdmaplkr  39181  rntrclfvOAI  39576  ismrcd1  39583  ismrcd2  39584  isnacs3  39595  nacsfix  39597  rgspnid  40060  iocinico  40106  harval3  40188  mptrcllem  40257  clcnvlem  40267  dmtrcl  40271  rntrcl  40272  cbviuneq12df  40306  dfrcl2  40319  dftrcl3  40365  brtrclfv2  40372  dfrtrcl3  40378  scottrankd  40904  nzin  40970  iunincfi  41680  founiiun  41754  founiiun0  41769  inmap  41790  difmapsn  41793  funimaeq  41836  iuneqfzuz  41920  supminfrnmpt  42035  supminfxr2  42061  supminfxrrnmpt  42063  iooiinicc  42132  icomnfinre  42142  iooiinioc  42146  limsupresxr  42361  liminfresxr  42362  limsup10exlem  42367  liminfvalxr  42378  fourierdlem79  42780  rrxsnicc  42895  prsal  42913  issalgend  42931  sge0f1o  42974  caragenuni  43103  caragendifcl  43106  opnvonmbllem2  43225  iinhoiicc  43266  pimconstlt1  43293  pimltpnf  43294  pimiooltgt  43299  pimgtmnf2  43302  pimdecfgtioc  43303  pimincfltioc  43304  pimdecfgtioo  43305  pimincfltioo  43306  preimageiingt  43308  preimaleiinlt  43309  sssmf  43325  smflimlem5  43361  smfmullem4  43379  smfpimbor1lem2  43384  smfsuplem1  43395  fzoopth  43837  sprsymrelf1  43966  lspeqlco  44801  setrecsres  45184
  Copyright terms: Public domain W3C validator