Theorem eqssd 3585

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	⊢ (𝜑 → 𝐴 ⊆ 𝐵)
eqssd.2	⊢ (𝜑 → 𝐵 ⊆ 𝐴)

Assertion

Ref	Expression
eqssd	⊢ (𝜑 → 𝐴 = 𝐵)

Proof of Theorem eqssd

Step	Hyp	Ref	Expression
1		eqssd.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		eqssd.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐴)
3		eqss 3583	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
4	1, 2, 3	sylanbrc 695	1 ⊢ (𝜑 → 𝐴 = 𝐵)

Syntax hints:   → wi 4   = wceq 1475   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554

This theorem is referenced by:  eqrd  3586  uneqdifeq  4009  uneqdifeqOLD  4010  unissel  4404  intmin  4432  unissint  4436  int0el  4443  dmcosseq  5308  sofld  5500  relfld  5578  preddowncl  5624  wfi  5630  tz7.7  5666  fimacnv  6255  knatar  6507  sorpssuni  6844  sorpssint  6845  onint  6887  fo2ndf  7171  suppimacnv  7193  tposeq  7241  wfrlem10  7311  onfununi  7325  tfrlem15  7375  oaass  7528  odi  7546  omass  7547  oelim2  7562  oeeui  7569  nnawordex  7604  oaabslem  7610  oaabs2  7612  omabslem  7613  omabs  7614  uniinqs  7714  sucdom2  8041  fineqv  8060  dffi2  8212  fiuni  8217  dffi3  8220  ordtypelem9  8314  ordtypelem10  8315  oismo  8328  hartogslem1  8330  ixpiunwdom  8379  cantnfp1lem3  8460  oemapvali  8464  cantnf  8473  r1val1  8532  rankval3b  8572  rankunb  8596  rankuni2b  8599  rankr1id  8608  rankc2  8617  rankxplim  8625  tcrank  8630  carden2b  8676  harval2  8706  en2other2  8715  infpwfien  8768  coflim  8966  cfcof  8979  cfidm  8980  isf32lem2  9059  fin1a2lem11  9115  fin1a2lem13  9117  ttukeylem7  9220  fpwwe2  9344  winafp  9398  wuncidm  9447  wuncval2  9448  tskuni  9484  grur1  9521  distrpr  9729  prlem934  9734  ltexpri  9744  reclem4pr  9751  fzopth  12249  fzosplit  12370  fzouzsplit  12372  ccatrn  13225  cotrtrclfv  13601  dmtrclfv  13607  dfrtrcl2  13650  phimullem  15322  prmreclem5  15462  structcnvcnv  15706  imasaddfnlem  16011  imasvscafn  16020  mrcuni  16104  mressmrcd  16110  submrc  16111  ssceq  16309  rescabs  16316  setcepi  16561  clatl  16939  ipopos  16983  psdmrn  17030  psssdm2  17038  dirdm  17057  gsumress  17099  gsumvallem2  17195  gsumwspan  17206  cycsubg  17445  conjnmz  17517  pmtrprfv  17696  symggen  17713  odf1o2  17811  gex1  17829  sylow2alem1  17855  sylow3lem3  17867  lsmidm  17900  lsmss1  17902  lsmss2  17904  lsmmod  17911  lsmdisj  17917  lsmdisj2  17918  cntzcmn  18068  prmcyg  18118  dmdprdd  18221  dprdspan  18249  dprdres  18250  dprdz  18252  subgdmdprd  18256  subgdprd  18257  dprddisj2  18261  dprd2dlem1  18263  dprd2da  18264  dmdprdsplit2lem  18267  dprdsplit  18270  ablfacrp  18288  pgpfac1lem3  18299  kerf1hrm  18566  isdrng2  18580  issubdrg  18628  lspun  18808  lspsn  18823  lspsnneg  18827  lsp0  18830  lsslsp  18836  lmhmlsp  18870  lspextmo  18877  lsmsp  18907  lspprabs  18916  lspsnvs  18935  lspdisj  18946  lsmcv  18962  lspsnat  18966  lsppratlem6  18973  lspprat  18974  lbsextlem4  18982  lidl1el  19039  drngnidl  19050  lidldvgen  19076  fidomndrng  19128  mplbas2  19291  cnsubrg  19625  mulgrhm2  19666  znrrg  19733  ocvin  19837  ocvlsp  19839  mrccss  19857  pjfo  19878  obs2ss  19892  frlmsslsp  19954  topsn  20550  eltg4i  20575  unitg  20582  tgtop  20588  tgidm  20595  en2top  20600  basgen  20603  2basgen  20605  fctop  20618  cctop  20620  ppttop  20621  epttop  20623  ntrin  20675  isopn3  20680  opnnei  20734  neiuni  20736  maxlp  20761  clslp  20762  tgrest  20773  resttopon  20775  rest0  20783  restfpw  20793  restcls  20795  restntr  20796  ordtbas2  20805  ordtbas  20806  ordtrest2  20818  cmpcov2  21003  tgcmp  21014  cmpcld  21015  uncmp  21016  cmpfi  21021  2ndcsep  21072  dis2ndc  21073  restnlly  21095  dislly  21110  comppfsc  21145  kgentopon  21151  kgencmp  21158  kgenidm  21160  iskgen2  21161  kgencn3  21171  ptuni2  21189  ptbasfi  21194  xkouni  21212  txcls  21217  ptclsg  21228  txdis  21245  txindis  21247  txcmplem2  21255  xkopt  21268  txcon  21302  qtopval2  21309  qtopuni  21315  qtoprest  21330  qtopomap  21331  qtopcmap  21332  kqsat  21344  kqcldsat  21346  hmeocls  21381  hmeontr  21382  hmphdis  21409  fgfil  21489  fgabs  21493  trfil1  21500  fgtr  21504  trfg  21505  uzrest  21511  ufilmax  21521  ufileu  21533  filufint  21534  ufildom1  21540  rnelfm  21567  flimfil  21583  uffclsflim  21645  alexsublem  21658  alexsubALTlem3  21663  alexsubALT  21665  ptcmplem2  21667  ptcmplem3  21668  tgpconcompeqg  21725  haustsms2  21750  tgptsmscls  21763  ust0  21833  ustbas2  21839  restutopopn  21852  unirnblps  22034  unirnbl  22035  iccntr  22432  pi1xfrcnv  22665  clsocv  22857  cfilfcls  22880  equivcmet  22922  pjth  23018  hlhil  23022  evthicc2  23036  ovolshft  23086  volsup  23131  dyadmbllem  23173  opnmbllem  23175  mbfconstlem  23202  itg11  23264  limciun  23464  dvidlem  23485  dvnres  23500  cpnord  23504  dvaddf  23511  dvmulf  23512  dvcmulf  23514  dvcof  23517  dvcj  23519  dvrec  23524  dvmptcmul  23533  dvcnv  23544  dvcnvre  23586  ftc1cn  23610  plyco0  23752  taylthlem1  23931  taylthlem2  23932  ulmdvlem3  23960  ulmdv  23961  pserdv  23987  wilthlem2  24595  ppisval  24630  ppisval2  24631  ppinprm  24678  chtnprm  24680  upgrex  25759  umgraex  25852  ubthlem1  27110  pjhth  27636  ococin  27651  chsupsn  27656  ssjo  27690  chabs1  27759  spansncvi  27895  mdslj1i  28562  mdslj2i  28563  atomli  28625  atcvatlem  28628  atcvat3i  28639  sumdmdlem  28661  reff  29234  cmpcref  29245  xpinpreima2  29281  ordtrest2NEW  29297  sigagenid  29541  imambfm  29651  dya2iocuni  29672  bnj1136  30319  bnj1398  30356  bnj1408  30358  bnj1498  30383  sconpi1  30475  cvmsss2  30510  cvmliftlem15  30534  dftrpred3g  30977  trpredpo  30979  frind  30984  sltval2  31053  nofulllem5  31105  altopthsn  31238  opnbnd  31490  opnregcld  31495  cldregopn  31496  fnessref  31522  neibastop1  31524  topmeet  31529  topjoin  31530  fnemeet1  31531  fnejoin1  31533  bj-restpw  32226  bj-restb  32228  bj-restuni2  32232  dissneqlem  32363  lindsenlbs  32574  poimirlem13  32592  poimirlem14  32593  poimirlem15  32594  opnmbllem0  32615  ftc1cnnc  32654  fdc  32711  sstotbnd2  32743  isbnd2  32752  totbndbnd  32758  prdstotbnd  32763  heibor1  32779  1idl  32995  igenval2  33035  lshpdisj  33292  lssats  33317  lsatcvat3  33357  lkrlsp  33407  lshpset2N  33424  lfl1dim  33426  lfl1dim2N  33427  lkrpssN  33468  paddass  34142  paddidm  34145  pmod1i  34152  pmapjat1  34157  pclbtwnN  34201  pclunN  34202  paddunN  34231  pclfinclN  34254  cdleme50rnlem  34850  dihjust  35524  dihmeetlem1N  35597  dihglblem5apreN  35598  dihmeetlem13N  35626  dochocsp  35686  dochdmj1  35697  dochnoncon  35698  dihjatb  35723  dihjat1lem  35735  lcfl9a  35812  lclkrlem2s  35832  lclkrlem2v  35835  mapdrvallem3  35953  mapdunirnN  35957  mapdin  35969  mapdlsm  35971  baerlem3lem2  36017  baerlem5alem2  36018  baerlem5blem2  36019  hdmaprnN  36174  hgmaprnN  36211  hdmaplkr  36223  rntrclfvOAI  36272  ismrcd1  36279  ismrcd2  36280  isnacs3  36291  nacsfix  36293  kercvrlsm  36671  pwssplit4  36677  hbtlem5  36717  rgspnid  36761  iocinico  36816  mptrcllem  36939  clcnvlem  36949  dmtrcl  36953  rntrcl  36954  cbviuneq12df  36972  dfrcl2  36985  dftrcl3  37031  brtrclfv2  37038  dfrtrcl3  37044  nzin  37539  iunincfi  38300  restuni3  38333  founiiun  38355  founiiun0  38372  disjf1o  38373  inmap  38396  difmapsn  38399  unirnmapsn  38401  iunmapsn  38404  iuneqfzuz  38492  icoiccdif  38597  iccdificc  38613  iooiinicc  38616  icomnfinre  38626  iooiinioc  38630  lptioo2  38698  lptioo1  38699  fourierdlem79  39078  rrxbasefi  39179  qndenserrn  39195  rrxsnicc  39196  intsaluni  39223  issalgend  39232  sge0f1o  39275  iundjiun  39353  meadjiunlem  39358  meaiininclem  39376  caragenuni  39401  caragendifcl  39404  opnvonmbllem2  39523  iinhoiicc  39565  iunhoiioo  39567  pimconstlt1  39592  pimltpnf  39593  pimiooltgt  39598  pimgtmnf2  39601  pimdecfgtioc  39602  pimincfltioc  39603  pimdecfgtioo  39604  pimincfltioo  39605  preimageiingt  39607  preimaleiinlt  39608  sssmf  39625  smflimlem5  39661  smfmullem4  39679  smfpimbor1lem2  39684  fzoopth  40360  uvtxnbgr  40627  nbupgruvtxres  40634  cplgruvtxb  40637  cusgredg  40646  lspeqlco  42022