Theorem eqssd 3361

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

Syntax hints:   -> wi 4   = wceq 1362   C_ wss 3316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-in 3323  df-ss 3330

This theorem is referenced by:  eqrd  3362  uneqdifeq  3755  unissel  4110  intmin  4136  unissint  4140  int0el  4147  reusv6OLD  4491  tz7.7  4732  dmcosseq  5088  sofld  5274  relfld  5351  fimacnv  5823  knatar  6035  sorpssuni  6358  sorpssint  6359  onint  6395  fo2ndf  6668  suppimacnv  6690  tposeq  6736  onfununi  6788  tfrlem15  6837  oaass  6988  odi  7006  omass  7007  oelim2  7022  oeeui  7029  nnawordex  7064  oaabslem  7070  oaabs2  7072  omabslem  7073  omabs  7074  uniinqs  7168  sucdom2  7495  fineqv  7516  dffi2  7661  fiuni  7666  dffi3  7669  ordtypelem9  7728  ordtypelem10  7729  oismo  7742  hartogslem1  7744  ixpiunwdom  7794  cantnfp1lem3  7876  oemapvali  7880  cantnf  7889  cantnfp1lem3OLD  7902  cantnfOLD  7911  r1val1  7981  rankval3b  8021  rankunb  8045  rankuni2b  8048  rankr1id  8057  rankc2  8066  rankxplim  8074  tcrank  8079  carden2b  8125  harval2  8155  en2other2  8164  infpwfien  8220  coflim  8418  cfcof  8431  cfidm  8432  isf32lem2  8511  fin1a2lem11  8567  fin1a2lem13  8569  ttukeylem7  8672  fpwwe2  8797  winafp  8851  wuncidm  8900  wuncval2  8901  tskuni  8937  grur1  8974  distrpr  9184  prlem934  9189  ltexpri  9199  reclem4pr  9206  fzopth  11481  fzosplit  11565  fzouzsplit  11567  phimullem  13836  prmreclem5  13963  structcnvcnv  14167  imasaddfnlem  14448  imasvscafn  14457  mrcuni  14541  mressmrcd  14547  submrc  14548  ssceq  14721  rescabs  14728  setcepi  14938  clatl  15268  ipopos  15312  psdmrn  15359  psssdm2  15367  dirdm  15386  gsumvallem2  15482  gsumress  15486  gsumwspan  15503  cycsubg  15688  conjnmz  15759  pmtrprfv  15938  symggen  15955  odf1o2  16051  gex1  16069  sylow2alem1  16095  sylow3lem3  16107  lsmidm  16140  lsmss1  16142  lsmss2  16144  lsmmod  16151  lsmdisj  16157  lsmdisj2  16158  cntzcmn  16303  prmcyg  16349  dmdprdd  16454  dprdspan  16497  dprdres  16498  dprdz  16500  subgdmdprd  16504  subgdprd  16505  dprddisj2  16510  dprddisj2OLD  16511  dprd2dlem1  16513  dprd2da  16514  dmdprdsplit2lem  16517  dprdsplit  16520  ablfacrp  16540  pgpfac1lem3  16551  isdrng2  16765  issubdrg  16813  lspun  16989  lspsn  17004  lspsnneg  17008  lsp0  17011  lsslsp  17017  lmhmlsp  17051  lspextmo  17058  lsmsp  17088  lspprabs  17097  lspsnvs  17116  lspdisj  17127  lsmcv  17143  lspsnat  17147  lsppratlem6  17154  lspprat  17155  lbsextlem4  17163  lidl1el  17221  drngnidl  17232  lidldvgen  17258  fidomndrng  17300  mplbas2  17482  mplbas2OLD  17483  cnsubrg  17716  mulgrhm2  17768  mulgrhm2OLD  17771  znrrg  17839  ocvin  17940  ocvlsp  17942  mrccss  17960  pjfo  17981  obs2ss  17995  frlmsslsp  18064  frlmsslspOLD  18065  topsn  18381  eltg4i  18406  tgtop  18419  tgidm  18426  en2top  18431  basgen  18434  2basgen  18436  fctop  18449  cctop  18451  ppttop  18452  epttop  18454  ntrin  18506  isopn3  18511  opnnei  18565  neiuni  18567  maxlp  18592  clslp  18593  tgrest  18604  resttopon  18606  rest0  18614  restfpw  18624  restcls  18626  restntr  18627  ordtbas2  18636  ordtbas  18637  ordtrest2  18649  cmpcov2  18834  tgcmp  18845  cmpcld  18846  uncmp  18847  cmpfi  18852  bwthOLD  18855  2ndcsep  18904  dis2ndc  18905  restnlly  18927  dislly  18942  kgentopon  18952  kgencmp  18959  kgenidm  18961  iskgen2  18962  kgencn3  18972  ptuni2  18990  ptbasfi  18995  xkouni  19013  txcls  19018  ptclsg  19029  txdis  19046  txindis  19048  txcmplem2  19056  xkopt  19069  txcon  19103  qtopval2  19110  qtopuni  19116  qtoprest  19131  qtopomap  19132  qtopcmap  19133  kqsat  19145  kqcldsat  19147  hmeocls  19182  hmeontr  19183  hmphdis  19210  fgfil  19289  fgabs  19293  trfil1  19300  fgtr  19304  trfg  19305  uzrest  19311  ufilmax  19321  ufileu  19333  filufint  19334  ufildom1  19340  rnelfm  19367  flimfil  19383  uffclsflim  19445  alexsublem  19457  alexsubALTlem3  19462  alexsubALT  19464  ptcmplem2  19466  ptcmplem3  19467  tgpconcompeqg  19523  haustsms2  19548  tgptsmscls  19565  ust0  19635  ustbas2  19641  restutopopn  19654  unirnblps  19835  unirnbl  19836  iccntr  20239  pi1xfrcnv  20470  clsocv  20603  cfilfcls  20626  equivcmet  20667  pjth  20767  hlhil  20771  evthicc2  20785  ovolshft  20835  volsup  20878  dyadmbllem  20920  opnmbllem  20922  mbfconstlem  20948  itg11  21010  limciun  21210  dvidlem  21231  dvnres  21246  cpnord  21250  dvaddf  21257  dvmulf  21258  dvcmulf  21260  dvcof  21263  dvcj  21265  dvrec  21270  dvmptcmul  21279  dvcnv  21290  dvcnvre  21332  ftc1cn  21356  plyco0  21544  taylthlem1  21722  taylthlem2  21723  ulmdvlem3  21751  ulmdv  21752  pserdv  21778  wilthlem2  22291  ppisval  22325  ppisval2  22326  ppinprm  22374  chtnprm  22376  umgraex  23079  ubthlem1  24093  pjhth  24618  ococin  24633  chsupsn  24638  ssjo  24672  chabs1  24741  spansncvi  24877  mdslj1i  25545  mdslj2i  25546  atomli  25608  atcvatlem  25611  atcvat3i  25622  sumdmdlem  25644  kerf1hrm  26144  xpinpreima2  26190  ordtrest2NEW  26206  sigagenid  26447  imambfm  26530  dya2iocuni  26551  sconpi1  26975  cvmsss2  27010  cvmliftlem15  27034  dfrtrcl2  27196  preddowncl  27503  wfi  27514  dftrpred3g  27543  trpredpo  27545  frind  27550  wfrlem10  27579  sltval2  27643  nofulllem5  27693  altopthsn  27838  opnmbllem0  28268  ftc1cnnc  28307  opnbnd  28361  opnregcld  28366  cldregopn  28367  fnessref  28406  comppfsc  28420  neibastop1  28421  topmeet  28426  topjoin  28427  fnemeet1  28428  fnejoin1  28430  fdc  28482  sstotbnd2  28514  isbnd2  28523  totbndbnd  28529  prdstotbnd  28534  heibor1  28550  1idl  28667  igenval2  28707  ismrcd1  28876  ismrcd2  28877  isnacs3  28888  nacsfix  28890  kercvrlsm  29278  pwssplit4  29284  hbtlem5  29326  rgspnid  29371  iocinico  29429  fzoopth  30056  lspeqlco  30679  bnj1136  31687  bnj1398  31724  bnj1408  31726  bnj1498  31751  lshpdisj  32202  lssats  32227  lsatcvat3  32267  lkrlsp  32317  lshpset2N  32334  lfl1dim  32336  lfl1dim2N  32337  lkrpssN  32378  paddass  33052  paddidm  33055  pmod1i  33062  pmapjat1  33067  pclbtwnN  33111  pclunN  33112  paddunN  33141  pclfinclN  33164  cdleme50rnlem  33758  dihjust  34432  dihmeetlem1N  34505  dihglblem5apreN  34506  dihmeetlem13N  34534  dochocsp  34594  dochdmj1  34605  dochnoncon  34606  dihjatb  34631  dihjat1lem  34643  lcfl9a  34720  lclkrlem2s  34740  lclkrlem2v  34743  mapdrvallem3  34861  mapdunirnN  34865  mapdin  34877  mapdlsm  34879  baerlem3lem2  34925  baerlem5alem2  34926  baerlem5blem2  34927  hdmaprnN  35082  hgmaprnN  35119  hdmaplkr  35131