Theorem eqssd 3964

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 3962	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
4	1, 2, 3	sylanbrc 583	1 ⊢ (𝜑 → 𝐴 = 𝐵)

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930

This theorem is referenced by:  eqelssd  3968  uneqdifeq  4455  pweq  4579  unieq  4881  unissel  4904  intmin  4934  unissint  4938  int0el  4945  intidg  5419  dmcosseq  5933  sofld  6144  relfld  6232  preddowncl  6291  frpoind  6301  wfiOLD  6310  tz7.7  6348  fimacnvOLD  7026  knatar  7307  sorpssuni  7674  sorpssint  7675  onint  7730  fo2ndf  8058  suppimacnv  8110  tposeq  8164  frrlem14  8235  onfununi  8292  tfrlem15  8343  oaass  8513  odi  8531  omass  8532  oelim2  8547  oeeui  8554  nnawordex  8589  oaabslem  8598  oaabs2  8600  omabslem  8601  omabs  8602  cofon1  8623  uniinqs  8743  sucdom2OLD  9033  sucdom2  9157  onomeneq  9179  fineqv  9214  dffi2  9368  fiuni  9373  dffi3  9376  hartogslem1  9487  ixpiunwdom  9535  cantnfp1lem3  9625  oemapvali  9629  cantnf  9638  dfttrcl2  9669  frind  9695  r1val1  9731  rankval3b  9771  rankunb  9795  rankuni2b  9798  rankr1id  9807  rankc2  9816  rankxplim  9824  tcrank  9829  carden2b  9912  harval2  9942  en2other2  9954  infpwfien  10007  coflim  10206  cfcof  10219  cfidm  10220  isf32lem2  10299  fin1a2lem11  10355  fin1a2lem13  10357  ttukeylem7  10460  fpwwe2  10588  winafp  10642  wuncidm  10691  wuncval2  10692  tskuni  10728  grur1  10765  distrpr  10973  ltexpri  10988  reclem4pr  10995  fzopth  13488  fzosplit  13615  fzouzsplit  13617  ccatrn  14489  cotrtrclfv  14909  dmtrclfv  14915  dfrtrcl2  14959  structcnvcnv  17036  imasaddfnlem  17424  imasvscafn  17433  mrcuni  17515  mressmrcd  17521  submrc  17522  ssceq  17723  rescabs  17732  rescabsOLD  17733  setcepi  17988  clatl  18411  ipopos  18439  psdmrn  18476  dirdm  18503  gsumress  18551  gsumvallem2  18658  gsumwspan  18670  trivsubgd  18969  trivsubgsnd  18970  trivnsgd  18988  cycsubg  19015  conjnmz  19056  pmtrprfv  19249  symggen  19266  odf1o2  19369  gex1  19387  sylow2alem1  19413  smndlsmidm  19452  lsmss1  19461  lsmss2  19463  lsmmod  19471  lsmdisj  19477  lsmdisj2  19478  cntzcmn  19632  prmcyg  19685  dmdprdd  19792  dprdspan  19820  dprdres  19821  dprdz  19823  subgdmdprd  19827  subgdprd  19828  dprddisj2  19832  dprd2dlem1  19834  dprd2da  19835  dmdprdsplit2lem  19838  dprdsplit  19841  ablfacrp  19859  pgpfac1lem3  19870  kerf1ghm  20193  issubdrg  20296  lspun  20505  lspsn  20520  lspsnneg  20524  lsp0  20527  lsslsp  20533  lmhmlsp  20567  lspextmo  20574  lsmsp  20604  lspprabs  20613  lspsnvs  20634  lspdisj  20645  lsmcv  20661  lspsnat  20665  lsppratlem6  20672  lspprat  20673  lbsextlem4  20681  lidl1el  20747  drngnidl  20758  lidldvgen  20784  cnsubrg  20894  mulgrhm2  20936  znrrg  21009  ocvin  21115  ocvlsp  21117  mrccss  21135  topsn  22317  eltg4i  22347  unitg  22354  tgtop  22360  tgidm  22367  en2top  22372  basgen  22375  2basgen  22377  fctop  22391  cctop  22393  ppttop  22394  epttop  22396  ntrin  22449  isopn3  22454  opnnei  22508  neiuni  22510  maxlp  22535  clslp  22536  tgrest  22547  resttopon  22549  rest0  22557  restcls  22569  restntr  22570  ordtbas2  22579  ordtbas  22580  ordtrest2  22592  cmpcov2  22778  tgcmp  22789  cmpcld  22790  uncmp  22791  cmpfi  22796  dis2ndc  22848  restnlly  22870  dislly  22885  comppfsc  22920  kgentopon  22926  kgencmp  22933  kgenidm  22935  iskgen2  22936  kgencn3  22946  ptuni2  22964  ptbasfi  22969  xkouni  22987  txcls  22992  txdis  23020  txindis  23022  txcmplem2  23030  xkopt  23043  txconn  23077  qtopval2  23084  qtopuni  23090  qtoprest  23105  qtopomap  23106  qtopcmap  23107  kqsat  23119  kqcldsat  23121  hmeocls  23156  hmeontr  23157  hmphdis  23184  fgfil  23263  fgabs  23267  trfil1  23274  fgtr  23278  uzrest  23285  ufilmax  23295  ufileu  23307  filufint  23308  ufildom1  23314  rnelfm  23341  flimfil  23357  uffclsflim  23419  alexsublem  23432  alexsubALTlem3  23437  alexsubALT  23439  ptcmplem2  23441  ptcmplem3  23442  tgpconncompeqg  23500  haustsms2  23525  tgptsmscls  23538  ust0  23608  ustbas2  23614  iccntr  24221  pi1xfrcnv  24457  clsocv  24651  cfilfcls  24675  equivcmet  24718  hlhil  24844  evthicc2  24861  ovolshft  24912  volsup  24957  dyadmbllem  25000  mbfconstlem  25028  itg11  25092  limciun  25295  dvnres  25332  cpnord  25336  dvcmulf  25346  dvmptcmul  25365  dvcnvre  25420  plyco0  25590  taylthlem1  25769  taylthlem2  25770  ulmdvlem3  25798  wilthlem2  26455  ppisval  26490  ppinprm  26538  chtnprm  26540  sltval2  27041  noextenddif  27053  scutun12  27192  madebdaylemlrcut  27271  cofcut1  27282  upgrex  28106  uvtxnbgr  28411  cusgredg  28435  ubthlem1  29875  pjhth  30398  ococin  30413  chsupsn  30418  ssjo  30452  chabs1  30521  spansncvi  30657  mdslj1i  31324  mdslj2i  31325  atomli  31387  atcvatlem  31390  atcvat3i  31401  sumdmdlem  31423  difininv  31508  fnpreimac  31654  pmtrcnelor  32012  cycpmrn  32062  fldgenid  32157  1fldgenq  32160  rspidlid  32235  0ringidl  32277  dimkerim  32409  cmpcref  32520  zarcls1  32539  zarclssn  32543  zart0  32549  zarcmplem  32551  xpinpreima2  32577  ordtrest2NEW  32593  sigagenid  32839  imambfm  32951  reprinfz1  33324  bnj1136  33698  bnj1398  33735  bnj1408  33737  bnj1498  33762  fineqvacALT  33788  sconnpi1  33920  cvmliftlem15  33979  altopthsn  34622  opnbnd  34873  opnregcld  34878  cldregopn  34879  fnessref  34905  neibastop1  34907  topmeet  34912  topjoin  34913  fnemeet1  34914  fnejoin1  34916  bj-gabeqd  35480  bj-restpw  35636  bj-restb  35638  bj-restuni2  35642  dissneqlem  35884  pibt2  35961  lindsenlbs  36146  poimirlem13  36164  poimirlem14  36165  poimirlem15  36166  fdc  36277  sstotbnd2  36306  isbnd2  36315  totbndbnd  36321  prdstotbnd  36326  heibor1  36342  1idl  36558  igenval2  36598  idreseqidinxp  36843  disjdmqs  37339  lshpdisj  37522  lssats  37547  lsatcvat3  37587  lshpset2N  37654  lfl1dim  37656  lfl1dim2N  37657  lkrpssN  37698  paddass  38374  paddidm  38377  pmod1i  38384  pmapjat1  38389  pclbtwnN  38433  pclunN  38434  paddunN  38463  pclfinclN  38486  dihjust  39753  dihmeetlem1N  39826  dihglblem5apreN  39827  dihmeetlem13N  39855  dochocsp  39915  dochdmj1  39926  dochnoncon  39927  dihjatb  39952  dihjat1lem  39964  lcfl9a  40041  lclkrlem2s  40061  lclkrlem2v  40064  mapdrvallem3  40182  mapdunirnN  40186  mapdin  40198  mapdlsm  40200  baerlem3lem2  40246  baerlem5alem2  40247  baerlem5blem2  40248  hdmaplkr  40449  sticksstones11  40637  rntrclfvOAI  41072  ismrcd1  41079  ismrcd2  41080  isnacs3  41091  nacsfix  41093  rgspnid  41557  iocinico  41604  onsupmaxb  41631  onsssupeqcond  41673  oacl2g  41723  omabs2  41725  omcl2  41726  ofoaf  41748  onsucunifi  41763  naddwordnexlem4  41795  harval3  41932  mptrcllem  42007  clcnvlem  42017  dmtrcl  42021  rntrcl  42022  cbviuneq12df  42055  dfrcl2  42068  dftrcl3  42114  brtrclfv2  42121  dfrtrcl3  42127  scottrankd  42650  nzin  42720  iunincfi  43426  founiiun  43518  founiiun0  43531  inmap  43551  difmapsn  43554  funimaeq  43595  iuneqfzuz  43690  supminfrnmpt  43800  supminfxr2  43824  supminfxrrnmpt  43826  pimxrneun  43844  iooiinicc  43900  icomnfinre  43910  iooiinioc  43914  limsupresxr  44127  liminfresxr  44128  limsup10exlem  44133  liminfvalxr  44144  fourierdlem79  44546  rrxsnicc  44661  prsal  44679  issalgend  44699  sge0f1o  44743  caragenuni  44872  caragendifcl  44875  opnvonmbllem2  44994  iinhoiicc  45035  pimconstlt1  45063  pimltpnff  45064  pimiooltgt  45071  pimgtmnf2  45075  pimdecfgtioc  45076  pimincfltioc  45077  pimdecfgtioo  45078  pimincfltioo  45079  preimageiingt  45081  preimaleiinlt  45082  pimgtmnff  45083  sssmf  45099  smflimlem5  45136  smfmullem4  45155  smfpimbor1lem2  45160  smfsuplem1  45172  smfpimne2  45201  fsupdm  45203  finfdm  45207  fzoopth  45679  sprsymrelf1  45808  lspeqlco  46640  isclatd  47128  intubeu  47129  unilbeu  47130  setrecsres  47267