Theorem eqssi 3948

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

Syntax hints:   = wceq 1541   ⊆ wss 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ss 3916

This theorem is referenced by:  inv1  4349  unv  4350  intab  4930  intabs  5291  dmv  5869  0ima  6034  cnvrescnv  6150  find  7834  dftpos4  8184  dfom3  9547  dmttrcl  9621  rnttrcl  9622  tc2  9640  tcidm  9644  tc0  9645  rankuni  9766  rankval4  9770  djuunxp  9824  djuun  9829  ackbij1  10138  cfom  10165  fin23lem16  10236  itunitc  10322  inaprc  10737  nqerf  10831  dmrecnq  10869  dmaddsr  10986  dmmulsr  10987  axaddf  11046  axmulf  11047  dfnn2  12148  dfuzi  12574  unirnioo  13359  uzrdgfni  13875  0bits  16360  4sqlem19  16885  ledm  18506  lern  18507  efgsfo  19661  0frgp  19701  indiscld  23016  leordtval2  23137  lecldbas  23144  llyidm  23413  nllyidm  23414  toplly  23415  lly1stc  23421  txuni2  23490  txindis  23559  ust0  24145  qdensere  24694  xrtgioo  24732  zdis  24742  xrhmeo  24881  bndth  24894  ismbf3d  25592  dvef  25921  reeff1o  26394  efifo  26493  dvloglem  26594  logf1o2  26596  bday1s  27785  onsiso  28215  dfn0s2  28270  bdayn0sf1o  28305  dfnns2  28307  choc1  31318  shsidmi  31375  shsval2i  31378  omlsii  31394  chdmm1i  31468  chj1i  31480  chm0i  31481  shjshsi  31483  span0  31533  spanuni  31535  sshhococi  31537  spansni  31548  pjoml4i  31578  pjrni  31693  shatomistici  32352  sumdmdlem2  32410  rinvf1o  32623  sigapildsys  34186  sxbrsigalem0  34295  dya2iocucvr  34308  sxbrsigalem4  34311  sxbrsiga  34314  ballotth  34562  kur14lem6  35266  mrsubrn  35568  msubrn  35584  filnetlem3  36435  filnetlem4  36436  onint1  36504  oninhaus  36505  bj-rabtr  36985  bj-rabtrAUTO  36987  bj-disj2r  37083  bj-nuliotaALT  37113  bj-idres  37215  icoreunrn  37414  dmsucmap  38491  comptiunov2i  43813  unisnALT  45032  fsumiunss  45689  fourierdlem62  46280  fouriersw  46343  salexct  46446  salgencntex  46455