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

Theorem eqssd 3983
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 3981 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
41, 2, 3sylanbrc 583 1 (𝜑𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wss 3935
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3942  df-ss 3951
This theorem is referenced by:  eqelssd  3987  uneqdifeq  4436  unissel  4862  intmin  4889  unissint  4893  int0el  4900  dmcosseq  5838  sofld  6038  relfld  6120  preddowncl  6169  wfi  6175  tz7.7  6211  fimacnv  6832  knatar  7099  sorpssuni  7447  sorpssint  7448  onint  7498  fo2ndf  7808  suppimacnv  7832  tposeq  7885  onfununi  7969  tfrlem15  8019  oaass  8177  odi  8195  omass  8196  oelim2  8211  oeeui  8218  nnawordex  8253  oaabslem  8260  oaabs2  8262  omabslem  8263  omabs  8264  uniinqs  8367  sucdom2  8703  fineqv  8722  dffi2  8876  fiuni  8881  dffi3  8884  hartogslem1  8995  ixpiunwdom  9044  cantnfp1lem3  9132  oemapvali  9136  cantnf  9145  r1val1  9204  rankval3b  9244  rankunb  9268  rankuni2b  9271  rankr1id  9280  rankc2  9289  rankxplim  9297  tcrank  9302  carden2b  9385  harval2  9415  en2other2  9424  infpwfien  9477  coflim  9672  cfcof  9685  cfidm  9686  isf32lem2  9765  fin1a2lem11  9821  fin1a2lem13  9823  ttukeylem7  9926  fpwwe2  10054  winafp  10108  wuncidm  10157  wuncval2  10158  tskuni  10194  grur1  10231  distrpr  10439  ltexpri  10454  reclem4pr  10461  fzopth  12934  fzosplit  13060  fzouzsplit  13062  ccatrn  13933  cotrtrclfv  14362  dmtrclfv  14368  dfrtrcl2  14411  structcnvcnv  16487  imasaddfnlem  16791  imasvscafn  16800  mrcuni  16882  mressmrcd  16888  submrc  16889  ssceq  17086  rescabs  17093  setcepi  17338  clatl  17716  ipopos  17760  psdmrn  17807  dirdm  17834  gsumress  17882  gsumvallem2  17988  gsumwspan  18001  trivsubgd  18245  trivsubgsnd  18246  trivnsgd  18264  cycsubg  18291  conjnmz  18332  pmtrprfv  18512  symggen  18529  odf1o2  18629  gex1  18647  sylow2alem1  18673  smndlsmidm  18712  lsmidmOLD  18720  lsmss1  18722  lsmss2  18724  lsmmod  18732  lsmdisj  18738  lsmdisj2  18739  cntzcmn  18891  prmcyg  18945  dmdprdd  19052  dprdspan  19080  dprdres  19081  dprdz  19083  subgdmdprd  19087  subgdprd  19088  dprddisj2  19092  dprd2dlem1  19094  dprd2da  19095  dmdprdsplit2lem  19098  dprdsplit  19101  ablfacrp  19119  pgpfac1lem3  19130  kerf1ghm  19428  kerf1hrmOLD  19429  issubdrg  19491  lspun  19690  lspsn  19705  lspsnneg  19709  lsp0  19712  lsslsp  19718  lmhmlsp  19752  lspextmo  19759  lsmsp  19789  lspprabs  19798  lspsnvs  19817  lspdisj  19828  lsmcv  19844  lspsnat  19848  lsppratlem6  19855  lspprat  19856  lbsextlem4  19864  lidl1el  19921  drngnidl  19932  lidldvgen  19958  cnsubrg  20535  mulgrhm2  20576  znrrg  20642  ocvin  20748  ocvlsp  20750  mrccss  20768  topsn  21469  eltg4i  21498  unitg  21505  tgtop  21511  tgidm  21518  en2top  21523  basgen  21526  2basgen  21528  fctop  21542  cctop  21544  ppttop  21545  epttop  21547  ntrin  21599  isopn3  21604  opnnei  21658  neiuni  21660  maxlp  21685  clslp  21686  tgrest  21697  resttopon  21699  rest0  21707  restcls  21719  restntr  21720  ordtbas2  21729  ordtbas  21730  ordtrest2  21742  cmpcov2  21928  tgcmp  21939  cmpcld  21940  uncmp  21941  cmpfi  21946  dis2ndc  21998  restnlly  22020  dislly  22035  comppfsc  22070  kgentopon  22076  kgencmp  22083  kgenidm  22085  iskgen2  22086  kgencn3  22096  ptuni2  22114  ptbasfi  22119  xkouni  22137  txcls  22142  txdis  22170  txindis  22172  txcmplem2  22180  xkopt  22193  txconn  22227  qtopval2  22234  qtopuni  22240  qtoprest  22255  qtopomap  22256  qtopcmap  22257  kqsat  22269  kqcldsat  22271  hmeocls  22306  hmeontr  22307  hmphdis  22334  fgfil  22413  fgabs  22417  trfil1  22424  fgtr  22428  uzrest  22435  ufilmax  22445  ufileu  22457  filufint  22458  ufildom1  22464  rnelfm  22491  flimfil  22507  uffclsflim  22569  alexsublem  22582  alexsubALTlem3  22587  alexsubALT  22589  ptcmplem2  22591  ptcmplem3  22592  tgpconncompeqg  22649  haustsms2  22674  tgptsmscls  22687  ust0  22757  ustbas2  22763  iccntr  23358  pi1xfrcnv  23590  clsocv  23782  cfilfcls  23806  equivcmet  23849  hlhil  23975  evthicc2  23990  ovolshft  24041  volsup  24086  dyadmbllem  24129  mbfconstlem  24157  itg11  24221  limciun  24421  dvnres  24457  cpnord  24461  dvcmulf  24471  dvmptcmul  24490  dvcnvre  24545  plyco0  24711  taylthlem1  24890  taylthlem2  24891  ulmdvlem3  24919  wilthlem2  25574  ppisval  25609  ppinprm  25657  chtnprm  25659  upgrex  26805  uvtxnbgr  27110  cusgredg  27134  ubthlem1  28575  pjhth  29098  ococin  29113  chsupsn  29118  ssjo  29152  chabs1  29221  spansncvi  29357  mdslj1i  30024  mdslj2i  30025  atomli  30087  atcvatlem  30090  atcvat3i  30101  sumdmdlem  30123  difininv  30207  fnpreimac  30345  pmtrcnelor  30663  cycpmrn  30713  dimkerim  30923  cmpcref  31014  xpinpreima2  31050  ordtrest2NEW  31066  sigagenid  31310  imambfm  31420  reprinfz1  31793  bnj1136  32167  bnj1398  32204  bnj1408  32206  bnj1498  32231  sconnpi1  32384  cvmliftlem15  32443  dftrpred3g  32970  trpredpo  32972  frpoind  32978  frind  32983  frrlem14  33034  sltval2  33061  noextenddif  33073  scutun12  33169  altopthsn  33320  opnbnd  33571  opnregcld  33576  cldregopn  33577  fnessref  33603  neibastop1  33605  topmeet  33610  topjoin  33611  fnemeet1  33612  fnejoin1  33614  bj-restpw  34278  bj-restb  34280  bj-restuni2  34284  dissneqlem  34504  pibt2  34581  lindsenlbs  34769  poimirlem13  34787  poimirlem14  34788  poimirlem15  34789  fdc  34903  sstotbnd2  34935  isbnd2  34944  totbndbnd  34950  prdstotbnd  34955  heibor1  34971  1idl  35187  igenval2  35227  idreseqidinxp  35450  lshpdisj  36005  lssats  36030  lsatcvat3  36070  lshpset2N  36137  lfl1dim  36139  lfl1dim2N  36140  lkrpssN  36181  paddass  36856  paddidm  36859  pmod1i  36866  pmapjat1  36871  pclbtwnN  36915  pclunN  36916  paddunN  36945  pclfinclN  36968  dihjust  38235  dihmeetlem1N  38308  dihglblem5apreN  38309  dihmeetlem13N  38337  dochocsp  38397  dochdmj1  38408  dochnoncon  38409  dihjatb  38434  dihjat1lem  38446  lcfl9a  38523  lclkrlem2s  38543  lclkrlem2v  38546  mapdrvallem3  38664  mapdunirnN  38668  mapdin  38680  mapdlsm  38682  baerlem3lem2  38728  baerlem5alem2  38729  baerlem5blem2  38730  hdmaplkr  38931  qsalrel  39005  rntrclfvOAI  39168  ismrcd1  39175  ismrcd2  39176  isnacs3  39187  nacsfix  39189  rgspnid  39652  iocinico  39698  harval3  39784  mptrcllem  39853  clcnvlem  39863  dmtrcl  39867  rntrcl  39868  cbviuneq12df  39886  dfrcl2  39899  dftrcl3  39945  brtrclfv2  39952  dfrtrcl3  39958  scottrankd  40464  nzin  40530  iunincfi  41240  founiiun  41315  founiiun0  41331  inmap  41352  difmapsn  41355  funimaeq  41398  iuneqfzuz  41483  supminfrnmpt  41599  supminfxr2  41625  supminfxrrnmpt  41627  iooiinicc  41698  icomnfinre  41708  iooiinioc  41712  limsupresxr  41927  liminfresxr  41928  limsup10exlem  41933  liminfvalxr  41944  fourierdlem79  42351  rrxsnicc  42466  prsal  42484  issalgend  42502  sge0f1o  42545  caragenuni  42674  caragendifcl  42677  opnvonmbllem2  42796  iinhoiicc  42837  pimconstlt1  42864  pimltpnf  42865  pimiooltgt  42870  pimgtmnf2  42873  pimdecfgtioc  42874  pimincfltioc  42875  pimdecfgtioo  42876  pimincfltioo  42877  preimageiingt  42879  preimaleiinlt  42880  sssmf  42896  smflimlem5  42932  smfmullem4  42950  smfpimbor1lem2  42955  smfsuplem1  42966  fzoopth  43408  sprsymrelf1  43505  lspeqlco  44392  setrecsres  44702
  Copyright terms: Public domain W3C validator