Theorem eqssd 3435

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

Syntax hints:   -> wi 4   = wceq 1452   C_ wss 3390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-in 3397  df-ss 3404

This theorem is referenced by:  eqrd  3436  uneqdifeq  3847  unissel  4220  intmin  4246  unissint  4250  int0el  4257  dmcosseq  5102  sofld  5290  relfld  5368  preddowncl  5414  wfi  5420  tz7.7  5456  fimacnv  6027  knatar  6266  sorpssuni  6599  sorpssint  6600  onint  6641  fo2ndf  6922  suppimacnv  6944  tposeq  6993  wfrlem10  7063  onfununi  7078  tfrlem15  7128  oaass  7280  odi  7298  omass  7299  oelim2  7314  oeeui  7321  nnawordex  7356  oaabslem  7362  oaabs2  7364  omabslem  7365  omabs  7366  uniinqs  7461  sucdom2  7786  fineqv  7805  dffi2  7955  fiuni  7960  dffi3  7963  ordtypelem9  8059  ordtypelem10  8060  oismo  8073  hartogslem1  8075  ixpiunwdom  8124  cantnfp1lem3  8203  oemapvali  8207  cantnf  8216  r1val1  8275  rankval3b  8315  rankunb  8339  rankuni2b  8342  rankr1id  8351  rankc2  8360  rankxplim  8368  tcrank  8373  carden2b  8419  harval2  8449  en2other2  8458  infpwfien  8511  coflim  8709  cfcof  8722  cfidm  8723  isf32lem2  8802  fin1a2lem11  8858  fin1a2lem13  8860  ttukeylem7  8963  fpwwe2  9086  winafp  9140  wuncidm  9189  wuncval2  9190  tskuni  9226  grur1  9263  distrpr  9471  prlem934  9476  ltexpri  9486  reclem4pr  9493  fzopth  11861  fzosplit  11978  fzouzsplit  11980  ccatrn  12784  cotrtrclfv  13153  dmtrclfv  13159  dfrtrcl2  13202  phimullem  14806  prmreclem5  14943  structcnvcnv  15210  imasaddfnlem  15512  imasvscafn  15521  mrcuni  15605  mressmrcd  15611  submrc  15612  ssceq  15809  rescabs  15816  setcepi  16061  clatl  16440  ipopos  16484  psdmrn  16531  psssdm2  16539  dirdm  16558  gsumress  16597  gsumvallem2  16697  gsumwspan  16708  cycsubg  16923  conjnmz  16994  pmtrprfv  17172  symggen  17189  odf1o2  17300  gex1  17321  sylow2alem1  17347  sylow3lem3  17359  lsmidm  17392  lsmss1  17394  lsmss2  17396  lsmmod  17403  lsmdisj  17409  lsmdisj2  17410  cntzcmn  17558  prmcyg  17606  dmdprdd  17709  dprdspan  17738  dprdres  17739  dprdz  17741  subgdmdprd  17745  subgdprd  17746  dprddisj2  17750  dprd2dlem1  17752  dprd2da  17753  dmdprdsplit2lem  17756  dprdsplit  17759  ablfacrp  17777  pgpfac1lem3  17788  kerf1hrm  18049  isdrng2  18063  issubdrg  18111  lspun  18288  lspsn  18303  lspsnneg  18307  lsp0  18310  lsslsp  18316  lmhmlsp  18350  lspextmo  18357  lsmsp  18387  lspprabs  18396  lspsnvs  18415  lspdisj  18426  lsmcv  18442  lspsnat  18446  lsppratlem6  18453  lspprat  18454  lbsextlem4  18462  lidl1el  18519  drngnidl  18530  lidldvgen  18556  fidomndrng  18608  mplbas2  18771  cnsubrg  19105  mulgrhm2  19147  znrrg  19213  ocvin  19314  ocvlsp  19316  mrccss  19334  pjfo  19355  obs2ss  19369  frlmsslsp  19431  topsn  20027  eltg4i  20052  unitg  20059  tgtop  20066  tgidm  20073  en2top  20078  basgen  20081  2basgen  20083  fctop  20096  cctop  20098  ppttop  20099  epttop  20101  ntrin  20153  isopn3  20159  opnnei  20213  neiuni  20215  maxlp  20240  clslp  20241  tgrest  20252  resttopon  20254  rest0  20262  restfpw  20272  restcls  20274  restntr  20275  ordtbas2  20284  ordtbas  20285  ordtrest2  20297  cmpcov2  20482  tgcmp  20493  cmpcld  20494  uncmp  20495  cmpfi  20500  2ndcsep  20551  dis2ndc  20552  restnlly  20574  dislly  20589  comppfsc  20624  kgentopon  20630  kgencmp  20637  kgenidm  20639  iskgen2  20640  kgencn3  20650  ptuni2  20668  ptbasfi  20673  xkouni  20691  txcls  20696  ptclsg  20707  txdis  20724  txindis  20726  txcmplem2  20734  xkopt  20747  txcon  20781  qtopval2  20788  qtopuni  20794  qtoprest  20809  qtopomap  20810  qtopcmap  20811  kqsat  20823  kqcldsat  20825  hmeocls  20860  hmeontr  20861  hmphdis  20888  fgfil  20968  fgabs  20972  trfil1  20979  fgtr  20983  trfg  20984  uzrest  20990  ufilmax  21000  ufileu  21012  filufint  21013  ufildom1  21019  rnelfm  21046  flimfil  21062  uffclsflim  21124  alexsublem  21137  alexsubALTlem3  21142  alexsubALT  21144  ptcmplem2  21146  ptcmplem3  21147  tgpconcompeqg  21204  haustsms2  21229  tgptsmscls  21242  ust0  21312  ustbas2  21318  restutopopn  21331  unirnblps  21512  unirnbl  21513  iccntr  21917  pi1xfrcnv  22166  clsocv  22299  cfilfcls  22322  equivcmet  22363  pjth  22471  hlhil  22475  evthicc2  22489  ovolshft  22542  volsup  22588  dyadmbllem  22636  opnmbllem  22638  mbfconstlem  22664  itg11  22728  limciun  22928  dvidlem  22949  dvnres  22964  cpnord  22968  dvaddf  22975  dvmulf  22976  dvcmulf  22978  dvcof  22981  dvcj  22983  dvrec  22988  dvmptcmul  22997  dvcnv  23008  dvcnvre  23050  ftc1cn  23074  plyco0  23225  taylthlem1  23407  taylthlem2  23408  ulmdvlem3  23436  ulmdv  23437  pserdv  23463  wilthlem2  24073  ppisval  24109  ppisval2  24110  ppinprm  24158  chtnprm  24160  umgraex  25129  ubthlem1  26593  pjhth  27127  ococin  27142  chsupsn  27147  ssjo  27181  chabs1  27250  spansncvi  27386  mdslj1i  28053  mdslj2i  28054  atomli  28116  atcvatlem  28119  atcvat3i  28130  sumdmdlem  28152  reff  28740  cmpcref  28751  xpinpreima2  28787  ordtrest2NEW  28803  sigagenid  29047  imambfm  29157  dya2iocuni  29178  bnj1136  29878  bnj1398  29915  bnj1408  29917  bnj1498  29942  sconpi1  30034  cvmsss2  30069  cvmliftlem15  30093  dftrpred3g  30545  trpredpo  30547  frind  30552  sltval2  30614  nofulllem5  30666  altopthsn  30799  opnbnd  31052  opnregcld  31057  cldregopn  31058  fnessref  31084  neibastop1  31086  topmeet  31091  topjoin  31092  fnemeet1  31093  fnejoin1  31095  dissneqlem  31812  poimirlem13  32017  poimirlem14  32018  poimirlem15  32019  opnmbllem0  32040  ftc1cnnc  32080  fdc  32138  sstotbnd2  32170  isbnd2  32179  totbndbnd  32185  prdstotbnd  32190  heibor1  32206  1idl  32323  igenval2  32363  lshpdisj  32624  lssats  32649  lsatcvat3  32689  lkrlsp  32739  lshpset2N  32756  lfl1dim  32758  lfl1dim2N  32759  lkrpssN  32800  paddass  33474  paddidm  33477  pmod1i  33484  pmapjat1  33489  pclbtwnN  33533  pclunN  33534  paddunN  33563  pclfinclN  33586  cdleme50rnlem  34182  dihjust  34856  dihmeetlem1N  34929  dihglblem5apreN  34930  dihmeetlem13N  34958  dochocsp  35018  dochdmj1  35029  dochnoncon  35030  dihjatb  35055  dihjat1lem  35067  lcfl9a  35144  lclkrlem2s  35164  lclkrlem2v  35167  mapdrvallem3  35285  mapdunirnN  35289  mapdin  35301  mapdlsm  35303  baerlem3lem2  35349  baerlem5alem2  35350  baerlem5blem2  35351  hdmaprnN  35506  hgmaprnN  35543  hdmaplkr  35555  rntrclfvOAI  35604  ismrcd1  35611  ismrcd2  35612  isnacs3  35623  nacsfix  35625  kercvrlsm  36012  pwssplit4  36018  hbtlem5  36058  rgspnid  36109  iocinico  36167  mptrcllem  36291  clcnvlem  36301  dmtrcl  36305  rntrcl  36306  cbviuneq12df  36324  dfrcl2  36337  dftrcl3  36383  brtrclfv2  36390  dfrtrcl3  36396  nzin  36737  founiiun  37517  founiiun0  37536  disjf1o  37537  inmap  37562  difmapsn  37565  unirnmapsn  37567  iunmapsn  37570  iuneqfzuz  37645  icoiccdif  37721  iccdificc  37737  lptioo2  37808  lptioo1  37809  fourierdlem79  38161  rrxbasefi  38264  qndenserrn  38280  intsaluni  38300  issalgend  38309  sge0f1o  38338  iundjiun  38414  meadjiunlem  38419  caragenuni  38451  caragendifcl  38454  opnvonmbllem2  38573  fzoopth  39208  upgrex  39338  uvtxnbgr  39637  nbupgruvtxres  39644  cplgruvtxb  39647  cusgredg  39656  lspeqlco  40740