Theorem eqssi 3947

Description: Infer equality from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 9-Sep-1993.)

Hypotheses

Ref	Expression
eqssi.1	⊢ 𝐴 ⊆ 𝐵
eqssi.2	⊢ 𝐵 ⊆ 𝐴

Assertion

Ref	Expression
eqssi	⊢ 𝐴 = 𝐵

Proof of Theorem eqssi

Step	Hyp	Ref	Expression
1		eqssi.1	. 2 ⊢ 𝐴 ⊆ 𝐵
2		eqssi.2	. 2 ⊢ 𝐵 ⊆ 𝐴
3		eqss 3946	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
4	1, 2, 3	mpbir2an 724	1 ⊢ 𝐴 = 𝐵

This proof depends on syntax axioms:   = wceq 1570   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-ss 3916

This theorem is used by:  inv1  4348  unv  4349  intab  4938  intabs  5313  dmv  5906  0ima  6074  cnvrescnv  6189  find  7893  dftpos4  8244  dfom3  9627  dmttrcl  9701  rnttrcl  9702  tc2  9720  tcidm  9724  tc0  9725  rankuni  9846  rankval4  9850  djuunxp  9927  djuun  9932  ackbij1  10240  cfom  10267  fin23lem16  10338  itunitc  10424  inaprc  10846  nqerf  10940  dmrecnq  10978  dmaddsr  11095  dmmulsr  11096  axaddf  11155  axmulf  11156  dfnn2  12271  dfuzi  12713  unirnioo  13503  uzrdgfni  14023  sgnrn  15172  0bits  16530  4sqlem19  17056  ledm  18679  lern  18680  efgsfo  19867  0frgp  19907  indiscld  23317  leordtval2  23438  lecldbas  23445  llyidm  23715  nllyidm  23716  toplly  23717  lly1stc  23723  txuni2  23792  txindis  23861  ust0  24447  qdensere  24996  xrtgioo  25034  zdis  25044  xrhmeo  25175  bndth  25187  ismbf3d  25883  dvef  26208  reeff1o  26684  efifo  26785  dvloglem  26886  logf1o2  26888  bday1  28080  oniso  28537  dfn0s2  28598  bdayn0sf1o  28636  dfnns2  28638  choc1  31809  shsidmi  31866  shsval2i  31869  omlsii  31885  chdmm1i  31959  chj1i  31971  chm0i  31972  shjshsi  31974  span0  32024  spanuni  32026  sshhococi  32028  spansni  32039  pjoml4i  32069  pjrni  32184  shatomistici  32843  sumdmdlem2  32901  rinvf1o  33104  sigapildsys  34674  sxbrsigalem0  34783  dya2iocucvr  34796  sxbrsigalem4  34799  sxbrsiga  34802  ballotth  35050  kur14lem6  35791  mrsubrn  36093  msubrn  36109  filnetlem3  37000  filnetlem4  37001  onint1  37069  oninhaus  37070  ttcuniun  37130  ttciunun  37131  ttcuni  37133  dfttc4  37150  bj-rabtr  37675  bj-rabtrAUTO  37677  bj-disj2r  37773  bj-nuliotaALT  37803  bj-idres  37913  icoreunrn  38114  dmsucmap  39217  comptiunov2i  44547  unisnALT  45749  fsumiunss  46406  fourierdlem62  46997  fouriersw  47060  salexct  47163  salgencntex  47172