Theorem eqssd 3394

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 3392	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
4	1, 2, 3	sylanbrc 664	1 |- ( ph -> A = B )

Syntax hints:   -> wi 4   = wceq 1369   C_ wss 3349

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-in 3356  df-ss 3363

This theorem is referenced by:  eqrd  3395  uneqdifeq  3788  unissel  4143  intmin  4169  unissint  4173  int0el  4180  reusv6OLD  4524  tz7.7  4766  dmcosseq  5122  sofld  5307  relfld  5384  fimacnv  5856  knatar  6069  sorpssuni  6390  sorpssint  6391  onint  6427  fo2ndf  6700  suppimacnv  6722  tposeq  6768  onfununi  6823  tfrlem15  6872  oaass  7021  odi  7039  omass  7040  oelim2  7055  oeeui  7062  nnawordex  7097  oaabslem  7103  oaabs2  7105  omabslem  7106  omabs  7107  uniinqs  7201  sucdom2  7528  fineqv  7549  dffi2  7694  fiuni  7699  dffi3  7702  ordtypelem9  7761  ordtypelem10  7762  oismo  7775  hartogslem1  7777  ixpiunwdom  7827  cantnfp1lem3  7909  oemapvali  7913  cantnf  7922  cantnfp1lem3OLD  7935  cantnfOLD  7944  r1val1  8014  rankval3b  8054  rankunb  8078  rankuni2b  8081  rankr1id  8090  rankc2  8099  rankxplim  8107  tcrank  8112  carden2b  8158  harval2  8188  en2other2  8197  infpwfien  8253  coflim  8451  cfcof  8464  cfidm  8465  isf32lem2  8544  fin1a2lem11  8600  fin1a2lem13  8602  ttukeylem7  8705  fpwwe2  8831  winafp  8885  wuncidm  8934  wuncval2  8935  tskuni  8971  grur1  9008  distrpr  9218  prlem934  9223  ltexpri  9233  reclem4pr  9240  fzopth  11516  fzosplit  11603  fzouzsplit  11605  phimullem  13875  prmreclem5  14002  structcnvcnv  14206  imasaddfnlem  14487  imasvscafn  14496  mrcuni  14580  mressmrcd  14586  submrc  14587  ssceq  14760  rescabs  14767  setcepi  14977  clatl  15307  ipopos  15351  psdmrn  15398  psssdm2  15406  dirdm  15425  gsumvallem2  15522  gsumress  15528  gsumwspan  15545  cycsubg  15730  conjnmz  15801  pmtrprfv  15980  symggen  15997  odf1o2  16093  gex1  16111  sylow2alem1  16137  sylow3lem3  16149  lsmidm  16182  lsmss1  16184  lsmss2  16186  lsmmod  16193  lsmdisj  16199  lsmdisj2  16200  cntzcmn  16345  prmcyg  16391  dmdprdd  16503  dprdspan  16546  dprdres  16547  dprdz  16549  subgdmdprd  16553  subgdprd  16554  dprddisj2  16559  dprddisj2OLD  16560  dprd2dlem1  16562  dprd2da  16563  dmdprdsplit2lem  16566  dprdsplit  16569  ablfacrp  16589  pgpfac1lem3  16600  kerf1hrm  16853  isdrng2  16864  issubdrg  16912  lspun  17090  lspsn  17105  lspsnneg  17109  lsp0  17112  lsslsp  17118  lmhmlsp  17152  lspextmo  17159  lsmsp  17189  lspprabs  17198  lspsnvs  17217  lspdisj  17228  lsmcv  17244  lspsnat  17248  lsppratlem6  17255  lspprat  17256  lbsextlem4  17264  lidl1el  17322  drngnidl  17333  lidldvgen  17359  fidomndrng  17401  mplbas2  17573  mplbas2OLD  17574  cnsubrg  17895  mulgrhm2  17949  mulgrhm2OLD  17952  znrrg  18020  ocvin  18121  ocvlsp  18123  mrccss  18141  pjfo  18162  obs2ss  18176  frlmsslsp  18245  frlmsslspOLD  18246  topsn  18562  eltg4i  18587  tgtop  18600  tgidm  18607  en2top  18612  basgen  18615  2basgen  18617  fctop  18630  cctop  18632  ppttop  18633  epttop  18635  ntrin  18687  isopn3  18692  opnnei  18746  neiuni  18748  maxlp  18773  clslp  18774  tgrest  18785  resttopon  18787  rest0  18795  restfpw  18805  restcls  18807  restntr  18808  ordtbas2  18817  ordtbas  18818  ordtrest2  18830  cmpcov2  19015  tgcmp  19026  cmpcld  19027  uncmp  19028  cmpfi  19033  bwthOLD  19036  2ndcsep  19085  dis2ndc  19086  restnlly  19108  dislly  19123  kgentopon  19133  kgencmp  19140  kgenidm  19142  iskgen2  19143  kgencn3  19153  ptuni2  19171  ptbasfi  19176  xkouni  19194  txcls  19199  ptclsg  19210  txdis  19227  txindis  19229  txcmplem2  19237  xkopt  19250  txcon  19284  qtopval2  19291  qtopuni  19297  qtoprest  19312  qtopomap  19313  qtopcmap  19314  kqsat  19326  kqcldsat  19328  hmeocls  19363  hmeontr  19364  hmphdis  19391  fgfil  19470  fgabs  19474  trfil1  19481  fgtr  19485  trfg  19486  uzrest  19492  ufilmax  19502  ufileu  19514  filufint  19515  ufildom1  19521  rnelfm  19548  flimfil  19564  uffclsflim  19626  alexsublem  19638  alexsubALTlem3  19643  alexsubALT  19645  ptcmplem2  19647  ptcmplem3  19648  tgpconcompeqg  19704  haustsms2  19729  tgptsmscls  19746  ust0  19816  ustbas2  19822  restutopopn  19835  unirnblps  20016  unirnbl  20017  iccntr  20420  pi1xfrcnv  20651  clsocv  20784  cfilfcls  20807  equivcmet  20848  pjth  20948  hlhil  20952  evthicc2  20966  ovolshft  21016  volsup  21059  dyadmbllem  21101  opnmbllem  21103  mbfconstlem  21129  itg11  21191  limciun  21391  dvidlem  21412  dvnres  21427  cpnord  21431  dvaddf  21438  dvmulf  21439  dvcmulf  21441  dvcof  21444  dvcj  21446  dvrec  21451  dvmptcmul  21460  dvcnv  21471  dvcnvre  21513  ftc1cn  21537  plyco0  21682  taylthlem1  21860  taylthlem2  21861  ulmdvlem3  21889  ulmdv  21890  pserdv  21916  wilthlem2  22429  ppisval  22463  ppisval2  22464  ppinprm  22512  chtnprm  22514  umgraex  23279  ubthlem1  24293  pjhth  24818  ococin  24833  chsupsn  24838  ssjo  24872  chabs1  24941  spansncvi  25077  mdslj1i  25745  mdslj2i  25746  atomli  25808  atcvatlem  25811  atcvat3i  25822  sumdmdlem  25844  xpinpreima2  26359  ordtrest2NEW  26375  sigagenid  26616  imambfm  26699  dya2iocuni  26720  sconpi1  27150  cvmsss2  27185  cvmliftlem15  27209  dfrtrcl2  27372  preddowncl  27679  wfi  27690  dftrpred3g  27719  trpredpo  27721  frind  27726  wfrlem10  27755  sltval2  27819  nofulllem5  27869  altopthsn  28014  opnmbllem0  28453  ftc1cnnc  28492  opnbnd  28546  opnregcld  28551  cldregopn  28552  fnessref  28591  comppfsc  28605  neibastop1  28606  topmeet  28611  topjoin  28612  fnemeet1  28613  fnejoin1  28615  fdc  28667  sstotbnd2  28699  isbnd2  28708  totbndbnd  28714  prdstotbnd  28719  heibor1  28735  1idl  28852  igenval2  28892  ismrcd1  29060  ismrcd2  29061  isnacs3  29072  nacsfix  29074  kercvrlsm  29462  pwssplit4  29468  hbtlem5  29510  rgspnid  29555  iocinico  29613  fzoopth  30239  lspeqlco  30970  bnj1136  32084  bnj1398  32121  bnj1408  32123  bnj1498  32148  lshpdisj  32728  lssats  32753  lsatcvat3  32793  lkrlsp  32843  lshpset2N  32860  lfl1dim  32862  lfl1dim2N  32863  lkrpssN  32904  paddass  33578  paddidm  33581  pmod1i  33588  pmapjat1  33593  pclbtwnN  33637  pclunN  33638  paddunN  33667  pclfinclN  33690  cdleme50rnlem  34284  dihjust  34958  dihmeetlem1N  35031  dihglblem5apreN  35032  dihmeetlem13N  35060  dochocsp  35120  dochdmj1  35131  dochnoncon  35132  dihjatb  35157  dihjat1lem  35169  lcfl9a  35246  lclkrlem2s  35266  lclkrlem2v  35269  mapdrvallem3  35387  mapdunirnN  35391  mapdin  35403  mapdlsm  35405  baerlem3lem2  35451  baerlem5alem2  35452  baerlem5blem2  35453  hdmaprnN  35608  hgmaprnN  35645  hdmaplkr  35657