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

Theorem eqssd 3809
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 3807 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
41, 2, 3sylanbrc 574 1 (𝜑𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  wss 3763
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 2067  ax-7 2103  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-ext 2781
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 2060  df-clab 2789  df-cleq 2795  df-clel 2798  df-in 3770  df-ss 3777
This theorem is referenced by:  eqrdOLD  3812  eqelssd  3813  uneqdifeq  4247  unissel  4655  intmin  4682  unissint  4686  int0el  4693  dmcosseq  5582  sofld  5786  relfld  5869  preddowncl  5914  wfi  5920  tz7.7  5956  fimacnv  6563  knatar  6825  sorpssuni  7170  sorpssint  7171  onint  7219  fo2ndf  7512  suppimacnv  7534  tposeq  7583  onfununi  7668  tfrlem15  7718  oaass  7872  odi  7890  omass  7891  oelim2  7906  oeeui  7913  nnawordex  7948  oaabslem  7954  oaabs2  7956  omabslem  7957  omabs  7958  uniinqs  8056  sucdom2  8389  fineqv  8408  dffi2  8562  fiuni  8567  dffi3  8570  hartogslem1  8680  ixpiunwdom  8729  cantnfp1lem3  8818  oemapvali  8822  cantnf  8831  r1val1  8890  rankval3b  8930  rankunb  8954  rankuni2b  8957  rankr1id  8966  rankc2  8975  rankxplim  8983  tcrank  8988  carden2b  9070  harval2  9100  en2other2  9109  infpwfien  9162  coflim  9362  cfcof  9375  cfidm  9376  isf32lem2  9455  fin1a2lem11  9511  fin1a2lem13  9513  ttukeylem7  9616  fpwwe2  9744  winafp  9798  wuncidm  9847  wuncval2  9848  tskuni  9884  grur1  9921  distrpr  10129  ltexpri  10144  reclem4pr  10151  fzopth  12595  fzosplit  12719  fzouzsplit  12721  ccatrn  13580  cotrtrclfv  13970  dmtrclfv  13976  dfrtrcl2  14019  structcnvcnv  16076  imasaddfnlem  16387  imasvscafn  16396  mrcuni  16480  mressmrcd  16486  submrc  16487  ssceq  16684  rescabs  16691  setcepi  16936  clatl  17315  ipopos  17359  psdmrn  17406  dirdm  17433  gsumress  17475  gsumvallem2  17571  gsumwspan  17582  cycsubg  17818  conjnmz  17890  pmtrprfv  18068  symggen  18085  odf1o2  18183  gex1  18201  sylow2alem1  18227  lsmidm  18272  lsmss1  18274  lsmss2  18276  lsmmod  18283  lsmdisj  18289  lsmdisj2  18290  cntzcmn  18440  prmcyg  18490  dmdprdd  18594  dprdspan  18622  dprdres  18623  dprdz  18625  subgdmdprd  18629  subgdprd  18630  dprddisj2  18634  dprd2dlem1  18636  dprd2da  18637  dmdprdsplit2lem  18640  dprdsplit  18643  ablfacrp  18661  pgpfac1lem3  18672  kerf1hrm  18941  issubdrg  19003  lspun  19188  lspsn  19203  lspsnneg  19207  lsp0  19210  lsslsp  19216  lmhmlsp  19250  lspextmo  19257  lsmsp  19287  lspprabs  19296  lspsnvs  19315  lspdisj  19326  lsmcv  19343  lspsnat  19347  lsppratlem6  19355  lspprat  19356  lbsextlem4  19364  lidl1el  19421  drngnidl  19432  lidldvgen  19458  cnsubrg  20008  mulgrhm2  20049  znrrg  20115  ocvin  20222  ocvlsp  20224  mrccss  20242  topsn  20943  eltg4i  20972  unitg  20979  tgtop  20985  tgidm  20992  en2top  20997  basgen  21000  2basgen  21002  fctop  21016  cctop  21018  ppttop  21019  epttop  21021  ntrin  21073  isopn3  21078  opnnei  21132  neiuni  21134  maxlp  21159  clslp  21160  tgrest  21171  resttopon  21173  rest0  21181  restcls  21193  restntr  21194  ordtbas2  21203  ordtbas  21204  ordtrest2  21216  cmpcov2  21401  tgcmp  21412  cmpcld  21413  uncmp  21414  cmpfi  21419  dis2ndc  21471  restnlly  21493  dislly  21508  comppfsc  21543  kgentopon  21549  kgencmp  21556  kgenidm  21558  iskgen2  21559  kgencn3  21569  ptuni2  21587  ptbasfi  21592  xkouni  21610  txcls  21615  txdis  21643  txindis  21645  txcmplem2  21653  xkopt  21666  txconn  21700  qtopval2  21707  qtopuni  21713  qtoprest  21728  qtopomap  21729  qtopcmap  21730  kqsat  21742  kqcldsat  21744  hmeocls  21779  hmeontr  21780  hmphdis  21807  fgfil  21886  fgabs  21890  trfil1  21897  fgtr  21901  uzrest  21908  ufilmax  21918  ufileu  21930  filufint  21931  ufildom1  21937  rnelfm  21964  flimfil  21980  uffclsflim  22042  alexsublem  22055  alexsubALTlem3  22060  alexsubALT  22062  ptcmplem2  22064  ptcmplem3  22065  tgpconncompeqg  22122  haustsms2  22147  tgptsmscls  22160  ust0  22230  ustbas2  22236  iccntr  22831  pi1xfrcnv  23063  clsocv  23255  cfilfcls  23278  equivcmet  23320  hlhil  23420  evthicc2  23435  ovolshft  23486  volsup  23531  dyadmbllem  23574  mbfconstlem  23602  itg11  23666  limciun  23866  dvnres  23902  cpnord  23906  dvcmulf  23916  dvmptcmul  23935  dvcnvre  23990  plyco0  24156  taylthlem1  24335  taylthlem2  24336  ulmdvlem3  24364  wilthlem2  25003  ppisval  25038  ppinprm  25086  chtnprm  25088  upgrex  26195  uvtxnbgr  26517  cplgruvtxbOLD  26533  cusgredg  26542  ubthlem1  28048  pjhth  28574  ococin  28589  chsupsn  28594  ssjo  28628  chabs1  28697  spansncvi  28833  mdslj1i  29500  mdslj2i  29501  atomli  29563  atcvatlem  29566  atcvat3i  29577  sumdmdlem  29599  difininv  29673  cmpcref  30236  xpinpreima2  30272  ordtrest2NEW  30288  sigagenid  30533  imambfm  30643  reprinfz1  31019  bnj1136  31382  bnj1398  31419  bnj1408  31421  bnj1498  31446  sconnpi1  31538  cvmliftlem15  31597  dftrpred3g  32047  trpredpo  32049  frpoind  32055  frind  32058  sltval2  32124  noextenddif  32136  scutun12  32232  altopthsn  32383  opnbnd  32635  opnregcld  32640  cldregopn  32641  fnessref  32667  neibastop1  32669  topmeet  32674  topjoin  32675  fnemeet1  32676  fnejoin1  32678  bj-restpw  33350  bj-restb  33352  bj-restuni2  33356  dissneqlem  33498  lindsenlbs  33711  poimirlem13  33729  poimirlem14  33730  poimirlem15  33731  fdc  33846  sstotbnd2  33878  isbnd2  33887  totbndbnd  33893  prdstotbnd  33898  heibor1  33914  1idl  34130  igenval2  34170  idreseqidinxp  34390  lshpdisj  34761  lssats  34786  lsatcvat3  34826  lshpset2N  34893  lfl1dim  34895  lfl1dim2N  34896  lkrpssN  34937  paddass  35612  paddidm  35615  pmod1i  35622  pmapjat1  35627  pclbtwnN  35671  pclunN  35672  paddunN  35701  pclfinclN  35724  dihjust  36992  dihmeetlem1N  37065  dihglblem5apreN  37066  dihmeetlem13N  37094  dochocsp  37154  dochdmj1  37165  dochnoncon  37166  dihjatb  37191  dihjat1lem  37203  lcfl9a  37280  lclkrlem2s  37300  lclkrlem2v  37303  mapdrvallem3  37421  mapdunirnN  37425  mapdin  37437  mapdlsm  37439  baerlem3lem2  37485  baerlem5alem2  37486  baerlem5blem2  37487  hdmaplkr  37688  rntrclfvOAI  37750  ismrcd1  37757  ismrcd2  37758  isnacs3  37769  nacsfix  37771  rgspnid  38237  iocinico  38291  mptrcllem  38414  clcnvlem  38424  dmtrcl  38428  rntrcl  38429  cbviuneq12df  38447  dfrcl2  38460  dftrcl3  38506  brtrclfv2  38513  dfrtrcl3  38519  nzin  39011  iunincfi  39759  founiiun  39843  founiiun0  39860  inmap  39882  difmapsn  39885  funimaeq  39938  iuneqfzuz  40025  supminfrnmpt  40145  supminfxr2  40172  supminfxrrnmpt  40174  iooiinicc  40243  icomnfinre  40253  iooiinioc  40257  limsupresxr  40472  liminfresxr  40473  limsup10exlem  40478  liminfvalxr  40489  fourierdlem79  40875  rrxsnicc  40993  issalgend  41029  sge0f1o  41072  caragenuni  41201  caragendifcl  41204  opnvonmbllem2  41323  iinhoiicc  41364  pimconstlt1  41391  pimltpnf  41392  pimiooltgt  41397  pimgtmnf2  41400  pimdecfgtioc  41401  pimincfltioc  41402  pimdecfgtioo  41403  pimincfltioo  41404  preimageiingt  41406  preimaleiinlt  41407  sssmf  41423  smflimlem5  41459  smfmullem4  41477  smfpimbor1lem2  41482  smfsuplem1  41493  fzoopth  41906  sprsymrelf1  42308  lspeqlco  42790  setrecsres  43010
  Copyright terms: Public domain W3C validator