Theorem eqssi 3953

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 3952	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
4	1, 2, 3	mpbir2an 723	1 ⊢ 𝐴 = 𝐵

Syntax hints:   = wceq 1570   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3922

This theorem is referenced by:  inv1  4355  unv  4356  intab  4943  intabs  5319  dmv  5912  0ima  6080  cnvrescnv  6194  find  7888  dftpos4  8237  dfom3  9612  dmttrcl  9686  rnttrcl  9687  tc2  9705  tcidm  9709  tc0  9710  rankuni  9831  rankval4  9835  djuunxp  9903  djuun  9908  ackbij1  10216  cfom  10243  fin23lem16  10314  itunitc  10400  inaprc  10816  nqerf  10910  dmrecnq  10948  dmaddsr  11065  dmmulsr  11066  axaddf  11125  axmulf  11126  dfnn2  12241  dfuzi  12682  unirnioo  13471  uzrdgfni  13990  sgnrn  15131  0bits  16492  4sqlem19  17018  ledm  18641  lern  18642  efgsfo  19804  0frgp  19844  indiscld  23248  leordtval2  23369  lecldbas  23376  llyidm  23645  nllyidm  23646  toplly  23647  lly1stc  23653  txuni2  23722  txindis  23791  ust0  24377  qdensere  24926  xrtgioo  24964  zdis  24974  xrhmeo  25105  bndth  25117  ismbf3d  25813  dvef  26139  reeff1o  26610  efifo  26712  dvloglem  26813  logf1o2  26815  bday1  28007  oniso  28464  dfn0s2  28525  bdayn0sf1o  28563  dfnns2  28565  choc1  31679  shsidmi  31736  shsval2i  31739  omlsii  31755  chdmm1i  31829  chj1i  31841  chm0i  31842  shjshsi  31844  span0  31894  spanuni  31896  sshhococi  31898  spansni  31909  pjoml4i  31939  pjrni  32054  shatomistici  32713  sumdmdlem2  32771  rinvf1o  32975  sigapildsys  34552  sxbrsigalem0  34661  dya2iocucvr  34674  sxbrsigalem4  34677  sxbrsiga  34680  ballotth  34928  kur14lem6  35703  mrsubrn  36005  msubrn  36021  filnetlem3  36911  filnetlem4  36912  onint1  36980  oninhaus  36981  ttcuniun  37041  ttciunun  37042  ttcuni  37044  dfttc4  37061  bj-rabtr  37586  bj-rabtrAUTO  37588  bj-disj2r  37684  bj-nuliotaALT  37714  bj-idres  37824  icoreunrn  38025  dmsucmap  39137  comptiunov2i  44452  unisnALT  45654  fsumiunss  46311  fourierdlem62  46902  fouriersw  46965  salexct  47068  salgencntex  47077