Theorem eqssi 3960

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

Syntax hints:   = wceq 1540   ⊆ wss 3911

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 2701

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

This theorem is referenced by:  inv1  4357  unv  4358  intab  4938  intabs  5299  intidOLD  5413  dmv  5876  0ima  6038  cnvrescnv  6156  find  7851  dftpos4  8201  dfom3  9576  dmttrcl  9650  rnttrcl  9651  tc2  9671  tcidm  9675  tc0  9676  rankuni  9792  rankval4  9796  djuunxp  9850  djuun  9855  ackbij1  10166  cfom  10193  fin23lem16  10264  itunitc  10350  inaprc  10765  nqerf  10859  dmrecnq  10897  dmaddsr  11014  dmmulsr  11015  axaddf  11074  axmulf  11075  dfnn2  12175  dfuzi  12601  unirnioo  13386  uzrdgfni  13899  0bits  16385  4sqlem19  16910  ledm  18531  lern  18532  efgsfo  19653  0frgp  19693  indiscld  23011  leordtval2  23132  lecldbas  23139  llyidm  23408  nllyidm  23409  toplly  23410  lly1stc  23416  txuni2  23485  txindis  23554  ust0  24140  qdensere  24690  xrtgioo  24728  zdis  24738  xrhmeo  24877  bndth  24890  ismbf3d  25588  dvef  25917  reeff1o  26390  efifo  26489  dvloglem  26590  logf1o2  26592  bday1s  27780  onsiso  28209  dfn0s2  28264  bdayn0sf1o  28299  dfnns2  28301  choc1  31306  shsidmi  31363  shsval2i  31366  omlsii  31382  chdmm1i  31456  chj1i  31468  chm0i  31469  shjshsi  31471  span0  31521  spanuni  31523  sshhococi  31525  spansni  31536  pjoml4i  31566  pjrni  31681  shatomistici  32340  sumdmdlem2  32398  rinvf1o  32604  sigapildsys  34145  sxbrsigalem0  34255  dya2iocucvr  34268  sxbrsigalem4  34271  sxbrsiga  34274  ballotth  34522  kur14lem6  35191  mrsubrn  35493  msubrn  35509  filnetlem3  36361  filnetlem4  36362  onint1  36430  oninhaus  36431  bj-rabtr  36911  bj-rabtrAUTO  36913  bj-disj2r  37009  bj-nuliotaALT  37039  bj-idres  37141  icoreunrn  37340  comptiunov2i  43688  unisnALT  44908  fsumiunss  45566  fourierdlem62  46159  fouriersw  46222  salexct  46325  salgencntex  46334