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

Theorem eqssd 3357
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  |-  ( ph  ->  A  C_  B )
eqssd.2  |-  ( ph  ->  B  C_  A )
Assertion
Ref Expression
eqssd  |-  ( ph  ->  A  =  B )

Proof of Theorem eqssd
StepHypRef Expression
1 eqssd.1 . 2  |-  ( ph  ->  A  C_  B )
2 eqssd.2 . 2  |-  ( ph  ->  B  C_  A )
3 eqss 3355 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
41, 2, 3sylanbrc 646 1  |-  ( ph  ->  A  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    C_ wss 3312
This theorem is referenced by:  eqrd  3358  uneqdifeq  3708  unissel  4036  intmin  4062  unissint  4066  int0el  4073  tz7.7  4599  reusv6OLD  4725  onint  4766  dmcosseq  5128  sofld  5309  relfld  5386  fimacnv  5853  knatar  6071  fo2ndf  6444  tposeq  6472  sorpssuni  6522  sorpssint  6523  onfununi  6594  tfrlem15  6644  oaass  6795  odi  6813  omass  6814  oelim2  6829  oeeui  6836  nnawordex  6871  oaabslem  6877  oaabs2  6879  omabslem  6880  omabs  6881  uniinqs  6975  sucdom2  7294  fineqv  7315  dffi2  7419  fiuni  7424  dffi3  7427  ordtypelem9  7484  ordtypelem10  7485  oismo  7498  hartogslem1  7500  ixpiunwdom  7548  cantnfp1lem3  7625  oemapvali  7629  cantnf  7638  r1val1  7701  rankval3b  7741  rankunb  7765  rankuni2b  7768  rankr1id  7777  rankc2  7786  rankxplim  7792  tcrank  7797  carden2b  7843  harval2  7873  infpwfien  7932  coflim  8130  cfcof  8143  cfidm  8144  isf32lem2  8223  fin1a2lem11  8279  fin1a2lem13  8281  ttukeylem7  8384  fpwwe2  8507  winafp  8561  wuncidm  8610  wuncval2  8611  tskuni  8647  grur1  8684  distrpr  8894  prlem934  8899  ltexpri  8909  reclem4pr  8916  fzopth  11078  fzosplit  11154  fzouzsplit  11156  phimullem  13156  prmreclem5  13276  structcnvcnv  13468  imasaddfnlem  13741  imasvscafn  13750  mrcuni  13834  mressmrcd  13840  submrc  13841  ssceq  14014  rescabs  14021  setcepi  14231  ipopos  14574  psdmrn  14627  psssdm2  14635  dirdm  14667  gsumvallem2  14760  gsumress  14765  gsumwspan  14779  cycsubg  14956  conjnmz  15027  odf1o2  15195  gex1  15213  sylow2alem1  15239  sylow3lem3  15251  lsmidm  15284  lsmss1  15286  lsmss2  15288  lsmmod  15295  lsmdisj  15301  lsmdisj2  15302  cntzcmn  15447  prmcyg  15491  dmdprdd  15548  dprdspan  15573  dprdres  15574  dprdz  15576  subgdmdprd  15580  subgdprd  15581  dprddisj2  15585  dprd2dlem1  15587  dprd2da  15588  dmdprdsplit2lem  15591  dprdsplit  15594  ablfacrp  15612  pgpfac1lem3  15623  isdrng2  15833  issubdrg  15881  lspun  16051  lspsn  16066  lspsnneg  16070  lsp0  16073  lsslsp  16079  lmhmlsp  16113  lspextmo  16120  lsmsp  16146  lspprabs  16155  lspsnvs  16174  lspdisj  16185  lsmcv  16201  lspsnat  16205  lsppratlem6  16212  lspprat  16213  lbsextlem4  16221  lidl1el  16277  drngnidl  16288  lidldvgen  16314  fidomndrng  16355  mplbas2  16519  cnsubrg  16747  mulgrhm2  16776  znrrg  16834  ocvin  16889  ocvlsp  16891  mrccss  16909  pjfo  16930  obs2ss  16944  topsn  16988  eltg4i  17013  tgtop  17026  tgidm  17033  en2top  17038  basgen  17041  2basgen  17043  fctop  17056  cctop  17058  ppttop  17059  epttop  17061  ntrin  17113  isopn3  17118  opnnei  17172  neiuni  17174  maxlp  17199  clslp  17200  tgrest  17211  resttopon  17213  rest0  17221  restfpw  17231  restcls  17233  restntr  17234  ordtbas2  17243  ordtbas  17244  ordtrest2  17256  cmpcov2  17441  tgcmp  17452  cmpcld  17453  uncmp  17454  cmpfi  17459  bwth  17461  2ndcsep  17510  dis2ndc  17511  restnlly  17533  dislly  17548  kgentopon  17558  kgencmp  17565  kgenidm  17567  iskgen2  17568  kgencn3  17578  ptuni2  17596  ptbasfi  17601  xkouni  17619  txcls  17624  ptclsg  17635  txdis  17652  txindis  17654  txcmplem2  17662  xkopt  17675  txcon  17709  qtopval2  17716  qtopuni  17722  qtoprest  17737  qtopomap  17738  qtopcmap  17739  kqsat  17751  kqcldsat  17753  hmeocls  17788  hmeontr  17789  hmphdis  17816  fgfil  17895  fgabs  17899  trfil1  17906  fgtr  17910  trfg  17911  uzrest  17917  ufilmax  17927  ufileu  17939  filufint  17940  ufildom1  17946  rnelfm  17973  flimfil  17989  uffclsflim  18051  alexsublem  18063  alexsubALTlem3  18068  alexsubALT  18070  ptcmplem2  18072  ptcmplem3  18073  tgpconcompeqg  18129  haustsms2  18154  tgptsmscls  18167  ust0  18237  ustbas2  18243  restutopopn  18256  unirnblps  18437  unirnbl  18438  iccntr  18840  pi1xfrcnv  19070  clsocv  19192  cfilfcls  19215  equivcmet  19256  pjth  19328  hlhil  19332  evthicc2  19345  ovolshft  19395  volsup  19438  dyadmbllem  19479  opnmbllem  19481  mbfconstlem  19509  itg11  19571  limciun  19769  dvidlem  19790  dvnres  19805  cpnord  19809  dvaddf  19816  dvmulf  19817  dvcmulf  19819  dvcof  19822  dvcj  19824  dvrec  19829  dvmptcmul  19838  dvcnv  19849  dvcnvre  19891  ftc1cn  19915  plyco0  20099  taylthlem1  20277  taylthlem2  20278  ulmdvlem3  20306  ulmdv  20307  pserdv  20333  wilthlem2  20840  ppisval  20874  ppisval2  20875  ppinprm  20923  chtnprm  20925  umgraex  21346  ubthlem1  22360  pjhth  22883  ococin  22898  chsupsn  22903  ssjo  22937  chabs1  23006  spansncvi  23142  mdslj1i  23810  mdslj2i  23811  atomli  23873  atcvatlem  23876  atcvat3i  23887  sumdmdlem  23909  kerf1hrm  24250  xpinpreima2  24293  sigagenid  24522  imambfm  24600  dya2iocuni  24621  sconpi1  24914  cvmsss2  24949  cvmliftlem15  24973  dfrtrcl2  25136  preddowncl  25451  wfi  25462  dftrpred3g  25491  trpredpo  25493  frind  25498  wfrlem10  25520  sltval2  25565  nofulllem5  25615  altopthsn  25754  mblfinlem  26190  ftc1cnnc  26225  opnbnd  26265  opnregcld  26270  cldregopn  26271  fnessref  26310  comppfsc  26324  neibastop1  26325  topmeet  26330  topjoin  26331  fnemeet1  26332  fnejoin1  26334  fdc  26386  sstotbnd2  26420  isbnd2  26429  totbndbnd  26435  prdstotbnd  26440  heibor1  26456  1idl  26573  igenval2  26613  ismrcd1  26689  ismrcd2  26690  isnacs3  26701  nacsfix  26703  kercvrlsm  27096  pwssplit4  27106  frlmsslsp  27163  hbtlem5  27247  rgspnid  27292  en2other2  27297  pmtrprfv  27311  symggen  27326  bnj1136  29220  bnj1398  29257  bnj1408  29259  bnj1498  29284  lshpdisj  29624  lssats  29649  lsatcvat3  29689  lkrlsp  29739  lshpset2N  29756  lfl1dim  29758  lfl1dim2N  29759  lkrpssN  29800  paddass  30474  paddidm  30477  pmod1i  30484  pmapjat1  30489  pclbtwnN  30533  pclunN  30534  paddunN  30563  pclfinclN  30586  cdleme50rnlem  31180  dihjust  31854  dihmeetlem1N  31927  dihglblem5apreN  31928  dihmeetlem13N  31956  dochocsp  32016  dochdmj1  32027  dochnoncon  32028  dihjatb  32053  dihjat1lem  32065  lcfl9a  32142  lclkrlem2s  32162  lclkrlem2v  32165  mapdrvallem3  32283  mapdunirnN  32287  mapdin  32299  mapdlsm  32301  baerlem3lem2  32347  baerlem5alem2  32348  baerlem5blem2  32349  hdmaprnN  32504  hgmaprnN  32541  hdmaplkr  32553
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator