Theorem eqssi 3952

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

Syntax hints:   = wceq 1560   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754  df-ss 3921

This theorem is referenced by:  inv1  4352  unv  4353  intab  4936  intabs  5305  dmv  5898  0ima  6067  cnvrescnv  6182  find  7876  dftpos4  8225  dfom3  9602  dmttrcl  9676  rnttrcl  9677  tc2  9695  tcidm  9699  tc0  9700  rankuni  9821  rankval4  9825  djuunxp  9879  djuun  9884  ackbij1  10193  cfom  10221  fin23lem16  10292  itunitc  10378  inaprc  10794  nqerf  10888  dmrecnq  10926  dmaddsr  11043  dmmulsr  11044  axaddf  11103  axmulf  11104  dfnn2  12223  dfuzi  12664  unirnioo  13453  uzrdgfni  13971  sgnrn  15111  0bits  16473  4sqlem19  16999  ledm  18622  lern  18623  efgsfo  19779  0frgp  19819  indiscld  23151  leordtval2  23272  lecldbas  23279  llyidm  23548  nllyidm  23549  toplly  23550  lly1stc  23556  txuni2  23625  txindis  23694  ust0  24280  qdensere  24829  xrtgioo  24867  zdis  24877  xrhmeo  25008  bndth  25020  ismbf3d  25716  dvef  26042  reeff1o  26510  efifo  26612  dvloglem  26713  logf1o2  26715  bday1  27907  oniso  28364  dfn0s2  28425  bdayn0sf1o  28463  dfnns2  28465  choc1  31530  shsidmi  31587  shsval2i  31590  omlsii  31606  chdmm1i  31680  chj1i  31692  chm0i  31693  shjshsi  31695  span0  31745  spanuni  31747  sshhococi  31749  spansni  31760  pjoml4i  31790  pjrni  31905  shatomistici  32564  sumdmdlem2  32622  rinvf1o  32832  sigapildsys  34459  sxbrsigalem0  34568  dya2iocucvr  34581  sxbrsigalem4  34584  sxbrsiga  34587  ballotth  34835  kur14lem6  35561  mrsubrn  35863  msubrn  35879  filnetlem3  36740  filnetlem4  36741  onint1  36809  oninhaus  36810  ttcuniun  36870  ttciunun  36871  ttcuni  36873  dfttc4  36890  bj-rabtr  37415  bj-rabtrAUTO  37417  bj-disj2r  37513  bj-nuliotaALT  37543  bj-idres  37652  icoreunrn  37853  dmsucmap  38967  comptiunov2i  44282  unisnALT  45501  fsumiunss  46151  fourierdlem62  46742  fouriersw  46805  salexct  46908  salgencntex  46917