Theorem eqssd 3620

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

Step	Hyp	Ref	Expression
1		eqssd.1	. 2 |- ( ph -> A C_ B )
2		eqssd.2	. 2 |- ( ph -> B C_ A )
3		eqss 3618	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
4	1, 2, 3	sylanbrc 698	1 |- ( ph -> A = B )

Syntax hints:   -> wi 4   = wceq 1483   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  eqrdOLD  3623  uneqdifeq  4057  uneqdifeqOLD  4058  unissel  4468  intmin  4497  unissint  4501  int0el  4508  dmcosseq  5387  sofld  5581  relfld  5661  preddowncl  5707  wfi  5713  tz7.7  5749  fimacnv  6347  knatar  6607  sorpssuni  6946  sorpssint  6947  onint  6995  fo2ndf  7284  suppimacnv  7306  tposeq  7354  wfrlem10  7424  onfununi  7438  tfrlem15  7488  oaass  7641  odi  7659  omass  7660  oelim2  7675  oeeui  7682  nnawordex  7717  oaabslem  7723  oaabs2  7725  omabslem  7726  omabs  7727  uniinqs  7827  sucdom2  8156  fineqv  8175  dffi2  8329  fiuni  8334  dffi3  8337  ordtypelem9  8431  ordtypelem10  8432  oismo  8445  hartogslem1  8447  ixpiunwdom  8496  cantnfp1lem3  8577  oemapvali  8581  cantnf  8590  r1val1  8649  rankval3b  8689  rankunb  8713  rankuni2b  8716  rankr1id  8725  rankc2  8734  rankxplim  8742  tcrank  8747  carden2b  8793  harval2  8823  en2other2  8832  infpwfien  8885  coflim  9083  cfcof  9096  cfidm  9097  isf32lem2  9176  fin1a2lem11  9232  fin1a2lem13  9234  ttukeylem7  9337  fpwwe2  9465  winafp  9519  wuncidm  9568  wuncval2  9569  tskuni  9605  grur1  9642  distrpr  9850  prlem934  9855  ltexpri  9865  reclem4pr  9872  fzopth  12378  fzosplit  12501  fzouzsplit  12503  ccatrn  13372  cotrtrclfv  13753  dmtrclfv  13759  dfrtrcl2  13802  phimullem  15484  prmreclem5  15624  structcnvcnv  15871  imasaddfnlem  16188  imasvscafn  16197  mrcuni  16281  mressmrcd  16287  submrc  16288  ssceq  16486  rescabs  16493  setcepi  16738  clatl  17116  ipopos  17160  psdmrn  17207  psssdm2  17215  dirdm  17234  gsumress  17276  gsumvallem2  17372  gsumwspan  17383  cycsubg  17622  conjnmz  17694  pmtrprfv  17873  symggen  17890  odf1o2  17988  gex1  18006  sylow2alem1  18032  sylow3lem3  18044  lsmidm  18077  lsmss1  18079  lsmss2  18081  lsmmod  18088  lsmdisj  18094  lsmdisj2  18095  cntzcmn  18245  prmcyg  18295  dmdprdd  18398  dprdspan  18426  dprdres  18427  dprdz  18429  subgdmdprd  18433  subgdprd  18434  dprddisj2  18438  dprd2dlem1  18440  dprd2da  18441  dmdprdsplit2lem  18444  dprdsplit  18447  ablfacrp  18465  pgpfac1lem3  18476  kerf1hrm  18743  isdrng2  18757  issubdrg  18805  lspun  18987  lspsn  19002  lspsnneg  19006  lsp0  19009  lsslsp  19015  lmhmlsp  19049  lspextmo  19056  lsmsp  19086  lspprabs  19095  lspsnvs  19114  lspdisj  19125  lsmcv  19141  lspsnat  19145  lsppratlem6  19152  lspprat  19153  lbsextlem4  19161  lidl1el  19218  drngnidl  19229  lidldvgen  19255  fidomndrng  19307  mplbas2  19470  cnsubrg  19806  mulgrhm2  19847  znrrg  19914  ocvin  20018  ocvlsp  20020  mrccss  20038  pjfo  20059  obs2ss  20073  frlmsslsp  20135  topsn  20735  eltg4i  20764  unitg  20771  tgtop  20777  tgidm  20784  en2top  20789  basgen  20792  2basgen  20794  fctop  20808  cctop  20810  ppttop  20811  epttop  20813  ntrin  20865  isopn3  20870  opnnei  20924  neiuni  20926  maxlp  20951  clslp  20952  tgrest  20963  resttopon  20965  rest0  20973  restfpw  20983  restcls  20985  restntr  20986  ordtbas2  20995  ordtbas  20996  ordtrest2  21008  cmpcov2  21193  tgcmp  21204  cmpcld  21205  uncmp  21206  cmpfi  21211  2ndcsep  21262  dis2ndc  21263  restnlly  21285  dislly  21300  comppfsc  21335  kgentopon  21341  kgencmp  21348  kgenidm  21350  iskgen2  21351  kgencn3  21361  ptuni2  21379  ptbasfi  21384  xkouni  21402  txcls  21407  ptclsg  21418  txdis  21435  txindis  21437  txcmplem2  21445  xkopt  21458  txconn  21492  qtopval2  21499  qtopuni  21505  qtoprest  21520  qtopomap  21521  qtopcmap  21522  kqsat  21534  kqcldsat  21536  hmeocls  21571  hmeontr  21572  hmphdis  21599  fgfil  21679  fgabs  21683  trfil1  21690  fgtr  21694  trfg  21695  uzrest  21701  ufilmax  21711  ufileu  21723  filufint  21724  ufildom1  21730  rnelfm  21757  flimfil  21773  uffclsflim  21835  alexsublem  21848  alexsubALTlem3  21853  alexsubALT  21855  ptcmplem2  21857  ptcmplem3  21858  tgpconncompeqg  21915  haustsms2  21940  tgptsmscls  21953  ust0  22023  ustbas2  22029  restutopopn  22042  unirnblps  22224  unirnbl  22225  iccntr  22624  pi1xfrcnv  22857  clsocv  23049  cfilfcls  23072  equivcmet  23114  pjth  23210  hlhil  23214  evthicc2  23229  ovolshft  23279  volsup  23324  dyadmbllem  23367  opnmbllem  23369  mbfconstlem  23396  itg11  23458  limciun  23658  dvidlem  23679  dvnres  23694  cpnord  23698  dvaddf  23705  dvmulf  23706  dvcmulf  23708  dvcof  23711  dvcj  23713  dvrec  23718  dvmptcmul  23727  dvcnv  23740  dvcnvre  23782  ftc1cn  23806  plyco0  23948  taylthlem1  24127  taylthlem2  24128  ulmdvlem3  24156  ulmdv  24157  pserdv  24183  wilthlem2  24795  ppisval  24830  ppisval2  24831  ppinprm  24878  chtnprm  24880  upgrex  25987  uvtxnbgr  26301  nbupgruvtxres  26308  cplgruvtxb  26311  cusgredg  26320  ubthlem1  27726  pjhth  28252  ococin  28267  chsupsn  28272  ssjo  28306  chabs1  28375  spansncvi  28511  mdslj1i  29178  mdslj2i  29179  atomli  29241  atcvatlem  29244  atcvat3i  29255  sumdmdlem  29277  difininv  29354  reff  29906  cmpcref  29917  xpinpreima2  29953  ordtrest2NEW  29969  sigagenid  30214  imambfm  30324  dya2iocuni  30345  reprinfz1  30700  bnj1136  31065  bnj1398  31102  bnj1408  31104  bnj1498  31129  sconnpi1  31221  cvmsss2  31256  cvmliftlem15  31280  dftrpred3g  31733  trpredpo  31735  frind  31740  sltval2  31809  noextenddif  31821  scutun12  31917  altopthsn  32068  opnbnd  32320  opnregcld  32325  cldregopn  32326  fnessref  32352  neibastop1  32354  topmeet  32359  topjoin  32360  fnemeet1  32361  fnejoin1  32363  bj-restpw  33045  bj-restb  33047  bj-restuni2  33051  dissneqlem  33187  lindsenlbs  33404  poimirlem13  33422  poimirlem14  33423  poimirlem15  33424  opnmbllem0  33445  ftc1cnnc  33484  fdc  33541  sstotbnd2  33573  isbnd2  33582  totbndbnd  33588  prdstotbnd  33593  heibor1  33609  1idl  33825  igenval2  33865  idreseqidinxp  34080  lshpdisj  34274  lssats  34299  lsatcvat3  34339  lkrlsp  34389  lshpset2N  34406  lfl1dim  34408  lfl1dim2N  34409  lkrpssN  34450  paddass  35124  paddidm  35127  pmod1i  35134  pmapjat1  35139  pclbtwnN  35183  pclunN  35184  paddunN  35213  pclfinclN  35236  cdleme50rnlem  35832  dihjust  36506  dihmeetlem1N  36579  dihglblem5apreN  36580  dihmeetlem13N  36608  dochocsp  36668  dochdmj1  36679  dochnoncon  36680  dihjatb  36705  dihjat1lem  36717  lcfl9a  36794  lclkrlem2s  36814  lclkrlem2v  36817  mapdrvallem3  36935  mapdunirnN  36939  mapdin  36951  mapdlsm  36953  baerlem3lem2  36999  baerlem5alem2  37000  baerlem5blem2  37001  hdmaprnN  37156  hgmaprnN  37193  hdmaplkr  37205  rntrclfvOAI  37254  ismrcd1  37261  ismrcd2  37262  isnacs3  37273  nacsfix  37275  kercvrlsm  37653  pwssplit4  37659  hbtlem5  37698  rgspnid  37742  iocinico  37797  mptrcllem  37920  clcnvlem  37930  dmtrcl  37934  rntrcl  37935  cbviuneq12df  37953  dfrcl2  37966  dftrcl3  38012  brtrclfv2  38019  dfrtrcl3  38025  nzin  38517  iunincfi  39272  restuni3  39301  founiiun  39360  founiiun0  39377  disjf1o  39378  inmap  39401  difmapsn  39404  unirnmapsn  39406  iunmapsn  39409  funimaeq  39461  iuneqfzuz  39551  supminfrnmpt  39672  supminfxr2  39699  supminfxrrnmpt  39701  icoiccdif  39750  iccdificc  39766  iooiinicc  39769  icomnfinre  39779  iooiinioc  39783  lptioo2  39863  lptioo1  39864  limsupresxr  39998  liminfresxr  39999  limsup10exlem  40004  liminfvalxr  40015  fourierdlem79  40402  rrxbasefi  40503  qndenserrn  40519  rrxsnicc  40520  intsaluni  40547  issalgend  40556  sge0f1o  40599  iundjiun  40677  meadjiunlem  40682  meaiininclem  40700  caragenuni  40725  caragendifcl  40728  opnvonmbllem2  40847  iinhoiicc  40888  iunhoiioo  40890  pimconstlt1  40915  pimltpnf  40916  pimiooltgt  40921  pimgtmnf2  40924  pimdecfgtioc  40925  pimincfltioc  40926  pimdecfgtioo  40927  pimincfltioo  40928  preimageiingt  40930  preimaleiinlt  40931  sssmf  40947  smflimlem5  40983  smfmullem4  41001  smfpimbor1lem2  41006  smfsuplem1  41017  fzoopth  41337  sprsymrelf1  41746  lspeqlco  42228