Theorem eqssd 3521

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

Syntax hints:   -> wi 4   = wceq 1379   C_ wss 3476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490

This theorem is referenced by:  eqrd  3522  uneqdifeq  3915  unissel  4276  intmin  4302  unissint  4306  int0el  4313  reusv6OLD  4658  tz7.7  4904  dmcosseq  5264  sofld  5455  relfld  5533  fimacnv  6013  knatar  6241  sorpssuni  6573  sorpssint  6574  onint  6614  fo2ndf  6890  suppimacnv  6912  tposeq  6957  onfununi  7012  tfrlem15  7061  oaass  7210  odi  7228  omass  7229  oelim2  7244  oeeui  7251  nnawordex  7286  oaabslem  7292  oaabs2  7294  omabslem  7295  omabs  7296  uniinqs  7391  sucdom2  7714  fineqv  7735  dffi2  7883  fiuni  7888  dffi3  7891  ordtypelem9  7951  ordtypelem10  7952  oismo  7965  hartogslem1  7967  ixpiunwdom  8017  cantnfp1lem3  8099  oemapvali  8103  cantnf  8112  cantnfp1lem3OLD  8125  cantnfOLD  8134  r1val1  8204  rankval3b  8244  rankunb  8268  rankuni2b  8271  rankr1id  8280  rankc2  8289  rankxplim  8297  tcrank  8302  carden2b  8348  harval2  8378  en2other2  8387  infpwfien  8443  coflim  8641  cfcof  8654  cfidm  8655  isf32lem2  8734  fin1a2lem11  8790  fin1a2lem13  8792  ttukeylem7  8895  fpwwe2  9021  winafp  9075  wuncidm  9124  wuncval2  9125  tskuni  9161  grur1  9198  distrpr  9406  prlem934  9411  ltexpri  9421  reclem4pr  9428  fzopth  11720  fzosplit  11826  fzouzsplit  11828  phimullem  14168  prmreclem5  14297  structcnvcnv  14501  imasaddfnlem  14783  imasvscafn  14792  mrcuni  14876  mressmrcd  14882  submrc  14883  ssceq  15056  rescabs  15063  setcepi  15273  clatl  15603  ipopos  15647  psdmrn  15694  psssdm2  15702  dirdm  15721  gsumvallem2  15823  gsumress  15829  gsumwspan  15846  cycsubg  16034  conjnmz  16105  pmtrprfv  16284  symggen  16301  odf1o2  16399  gex1  16417  sylow2alem1  16443  sylow3lem3  16455  lsmidm  16488  lsmss1  16490  lsmss2  16492  lsmmod  16499  lsmdisj  16505  lsmdisj2  16506  cntzcmn  16651  prmcyg  16699  dmdprdd  16833  dprdspan  16876  dprdres  16877  dprdz  16879  subgdmdprd  16883  subgdprd  16884  dprddisj2  16889  dprddisj2OLD  16890  dprd2dlem1  16892  dprd2da  16893  dmdprdsplit2lem  16896  dprdsplit  16899  ablfacrp  16919  pgpfac1lem3  16930  kerf1hrm  17192  isdrng2  17206  issubdrg  17254  lspun  17433  lspsn  17448  lspsnneg  17452  lsp0  17455  lsslsp  17461  lmhmlsp  17495  lspextmo  17502  lsmsp  17532  lspprabs  17541  lspsnvs  17560  lspdisj  17571  lsmcv  17587  lspsnat  17591  lsppratlem6  17598  lspprat  17599  lbsextlem4  17607  lidl1el  17665  drngnidl  17676  lidldvgen  17702  fidomndrng  17755  mplbas2  17933  mplbas2OLD  17934  cnsubrg  18274  mulgrhm2  18328  mulgrhm2OLD  18331  znrrg  18399  ocvin  18500  ocvlsp  18502  mrccss  18520  pjfo  18541  obs2ss  18555  frlmsslsp  18624  frlmsslspOLD  18625  topsn  19231  eltg4i  19256  tgtop  19269  tgidm  19276  en2top  19281  basgen  19284  2basgen  19286  fctop  19299  cctop  19301  ppttop  19302  epttop  19304  ntrin  19356  isopn3  19361  opnnei  19415  neiuni  19417  maxlp  19442  clslp  19443  tgrest  19454  resttopon  19456  rest0  19464  restfpw  19474  restcls  19476  restntr  19477  ordtbas2  19486  ordtbas  19487  ordtrest2  19499  cmpcov2  19684  tgcmp  19695  cmpcld  19696  uncmp  19697  cmpfi  19702  bwthOLD  19705  2ndcsep  19754  dis2ndc  19755  restnlly  19777  dislly  19792  kgentopon  19802  kgencmp  19809  kgenidm  19811  iskgen2  19812  kgencn3  19822  ptuni2  19840  ptbasfi  19845  xkouni  19863  txcls  19868  ptclsg  19879  txdis  19896  txindis  19898  txcmplem2  19906  xkopt  19919  txcon  19953  qtopval2  19960  qtopuni  19966  qtoprest  19981  qtopomap  19982  qtopcmap  19983  kqsat  19995  kqcldsat  19997  hmeocls  20032  hmeontr  20033  hmphdis  20060  fgfil  20139  fgabs  20143  trfil1  20150  fgtr  20154  trfg  20155  uzrest  20161  ufilmax  20171  ufileu  20183  filufint  20184  ufildom1  20190  rnelfm  20217  flimfil  20233  uffclsflim  20295  alexsublem  20307  alexsubALTlem3  20312  alexsubALT  20314  ptcmplem2  20316  ptcmplem3  20317  tgpconcompeqg  20373  haustsms2  20398  tgptsmscls  20415  ust0  20485  ustbas2  20491  restutopopn  20504  unirnblps  20685  unirnbl  20686  iccntr  21089  pi1xfrcnv  21320  clsocv  21453  cfilfcls  21476  equivcmet  21517  pjth  21617  hlhil  21621  evthicc2  21635  ovolshft  21685  volsup  21729  dyadmbllem  21771  opnmbllem  21773  mbfconstlem  21799  itg11  21861  limciun  22061  dvidlem  22082  dvnres  22097  cpnord  22101  dvaddf  22108  dvmulf  22109  dvcmulf  22111  dvcof  22114  dvcj  22116  dvrec  22121  dvmptcmul  22130  dvcnv  22141  dvcnvre  22183  ftc1cn  22207  plyco0  22352  taylthlem1  22530  taylthlem2  22531  ulmdvlem3  22559  ulmdv  22560  pserdv  22586  wilthlem2  23099  ppisval  23133  ppisval2  23134  ppinprm  23182  chtnprm  23184  umgraex  24027  ubthlem1  25490  pjhth  26015  ococin  26030  chsupsn  26035  ssjo  26069  chabs1  26138  spansncvi  26274  mdslj1i  26942  mdslj2i  26943  atomli  27005  atcvatlem  27008  atcvat3i  27019  sumdmdlem  27041  xpinpreima2  27553  ordtrest2NEW  27569  sigagenid  27819  imambfm  27901  dya2iocuni  27922  sconpi1  28352  cvmsss2  28387  cvmliftlem15  28411  dfrtrcl2  28574  preddowncl  28881  wfi  28892  dftrpred3g  28921  trpredpo  28923  frind  28928  wfrlem10  28957  sltval2  29021  nofulllem5  29071  altopthsn  29216  opnmbllem0  29655  ftc1cnnc  29694  opnbnd  29748  opnregcld  29753  cldregopn  29754  fnessref  29793  comppfsc  29807  neibastop1  29808  topmeet  29813  topjoin  29814  fnemeet1  29815  fnejoin1  29817  fdc  29869  sstotbnd2  29901  isbnd2  29910  totbndbnd  29916  prdstotbnd  29921  heibor1  29937  1idl  30054  igenval2  30094  ismrcd1  30262  ismrcd2  30263  isnacs3  30274  nacsfix  30276  kercvrlsm  30661  pwssplit4  30667  hbtlem5  30709  rgspnid  30754  iocinico  30812  nzin  30851  lptioo2  31201  lptioo1  31202  fourierdlem79  31514  fzoopth  31835  lspeqlco  32139  bnj1136  33150  bnj1398  33187  bnj1408  33189  bnj1498  33214  lshpdisj  33802  lssats  33827  lsatcvat3  33867  lkrlsp  33917  lshpset2N  33934  lfl1dim  33936  lfl1dim2N  33937  lkrpssN  33978  paddass  34652  paddidm  34655  pmod1i  34662  pmapjat1  34667  pclbtwnN  34711  pclunN  34712  paddunN  34741  pclfinclN  34764  cdleme50rnlem  35358  dihjust  36032  dihmeetlem1N  36105  dihglblem5apreN  36106  dihmeetlem13N  36134  dochocsp  36194  dochdmj1  36205  dochnoncon  36206  dihjatb  36231  dihjat1lem  36243  lcfl9a  36320  lclkrlem2s  36340  lclkrlem2v  36343  mapdrvallem3  36461  mapdunirnN  36465  mapdin  36477  mapdlsm  36479  baerlem3lem2  36525  baerlem5alem2  36526  baerlem5blem2  36527  hdmaprnN  36682  hgmaprnN  36719  hdmaplkr  36731