Theorem eqssi 3942

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

Syntax hints:   = wceq 1542   ⊆ wss 3892

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-v 3433  df-in 3899  df-ss 3909

This theorem is referenced by:  inv1  4334  unv  4335  intab  4915  intabs  5270  intid  5377  dmv  5830  0ima  5985  cnvrescnv  6097  find  7737  findOLD  7738  dftpos4  8052  wfrlem16OLD  8146  dfom3  9383  dmttrcl  9457  rnttrcl  9458  tc2  9500  tcidm  9504  tc0  9505  rankuni  9622  rankval4  9626  djuunxp  9680  djuun  9685  ackbij1  9995  cfom  10021  fin23lem16  10092  itunitc  10178  inaprc  10593  nqerf  10687  dmrecnq  10725  dmaddsr  10842  dmmulsr  10843  axaddf  10902  axmulf  10903  dfnn2  11986  dfuzi  12411  unirnioo  13180  uzrdgfni  13676  0bits  16144  4sqlem19  16662  ledm  18306  lern  18307  efgsfo  19343  0frgp  19383  indiscld  22240  leordtval2  22361  lecldbas  22368  llyidm  22637  nllyidm  22638  toplly  22639  lly1stc  22645  txuni2  22714  txindis  22783  ust0  23369  qdensere  23931  xrtgioo  23967  zdis  23977  xrhmeo  24107  bndth  24119  ismbf3d  24816  dvef  25142  reeff1o  25604  efifo  25701  dvloglem  25801  logf1o2  25803  choc1  29685  shsidmi  29742  shsval2i  29745  omlsii  29761  chdmm1i  29835  chj1i  29847  chm0i  29848  shjshsi  29850  span0  29900  spanuni  29902  sshhococi  29904  spansni  29915  pjoml4i  29945  pjrni  30060  shatomistici  30719  sumdmdlem2  30777  rinvf1o  30961  sigapildsys  32126  sxbrsigalem0  32234  dya2iocucvr  32247  sxbrsigalem4  32250  sxbrsiga  32253  ballotth  32500  kur14lem6  33169  mrsubrn  33471  msubrn  33487  bday1s  34021  filnetlem3  34565  filnetlem4  34566  onint1  34634  oninhaus  34635  bj-rabtr  35114  bj-rabtrAUTO  35116  bj-disj2r  35214  bj-nuliotaALT  35225  bj-idres  35327  icoreunrn  35526  comptiunov2i  41284  unisnALT  42516  fsumiunss  43087  fourierdlem62  43680  fouriersw  43743  salexct  43844  salgencntex  43853