Theorem eqssi 3980

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

Syntax hints:   = wceq 1540   ⊆ wss 3931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2728  df-ss 3948

This theorem is referenced by:  inv1  4378  unv  4379  intab  4959  intabs  5324  intidOLD  5438  dmv  5907  0ima  6070  cnvrescnv  6189  find  7896  dftpos4  8249  wfrlem16OLD  8343  dfom3  9666  dmttrcl  9740  rnttrcl  9741  tc2  9761  tcidm  9765  tc0  9766  rankuni  9882  rankval4  9886  djuunxp  9940  djuun  9945  ackbij1  10256  cfom  10283  fin23lem16  10354  itunitc  10440  inaprc  10855  nqerf  10949  dmrecnq  10987  dmaddsr  11104  dmmulsr  11105  axaddf  11164  axmulf  11165  dfnn2  12258  dfuzi  12689  unirnioo  13471  uzrdgfni  13981  0bits  16463  4sqlem19  16988  ledm  18605  lern  18606  efgsfo  19725  0frgp  19765  indiscld  23034  leordtval2  23155  lecldbas  23162  llyidm  23431  nllyidm  23432  toplly  23433  lly1stc  23439  txuni2  23508  txindis  23577  ust0  24163  qdensere  24713  xrtgioo  24751  zdis  24761  xrhmeo  24900  bndth  24913  ismbf3d  25612  dvef  25941  reeff1o  26414  efifo  26513  dvloglem  26614  logf1o2  26616  bday1s  27800  onsiso  28226  dfn0s2  28281  bdayn0sf1o  28316  dfnns2  28318  choc1  31313  shsidmi  31370  shsval2i  31373  omlsii  31389  chdmm1i  31463  chj1i  31475  chm0i  31476  shjshsi  31478  span0  31528  spanuni  31530  sshhococi  31532  spansni  31543  pjoml4i  31573  pjrni  31688  shatomistici  32347  sumdmdlem2  32405  rinvf1o  32613  sigapildsys  34198  sxbrsigalem0  34308  dya2iocucvr  34321  sxbrsigalem4  34324  sxbrsiga  34327  ballotth  34575  kur14lem6  35238  mrsubrn  35540  msubrn  35556  filnetlem3  36403  filnetlem4  36404  onint1  36472  oninhaus  36473  bj-rabtr  36953  bj-rabtrAUTO  36955  bj-disj2r  37051  bj-nuliotaALT  37081  bj-idres  37183  icoreunrn  37382  comptiunov2i  43705  unisnALT  44925  fsumiunss  45584  fourierdlem62  46177  fouriersw  46240  salexct  46343  salgencntex  46352