Theorem eqssi 3837

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

Syntax hints:   = wceq 1601   ⊆ wss 3792

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-in 3799  df-ss 3806

This theorem is referenced by:  inv1  4196  unv  4197  intab  4742  intabs  5061  intid  5160  dmv  5588  0ima  5738  find  7371  dftpos4  7655  wfrlem16  7715  dfom3  8843  tc2  8917  tcidm  8921  tc0  8922  rankuni  9025  rankval4  9029  djuunxp  9082  djuun  9087  ackbij1  9397  cfom  9423  fin23lem16  9494  itunitc  9580  inaprc  9995  nqerf  10089  dmrecnq  10127  dmaddsr  10244  dmmulsr  10245  axaddf  10304  axmulf  10305  dfnn2  11394  dfuzi  11825  unirnioo  12591  uzrdgfni  13081  0bits  15577  4sqlem19  16082  ledm  17621  lern  17622  efgsfo  18548  0frgp  18589  indiscld  21314  leordtval2  21435  lecldbas  21442  llyidm  21711  nllyidm  21712  toplly  21713  lly1stc  21719  txuni2  21788  txindis  21857  ust0  22442  qdensere  22992  xrtgioo  23028  zdis  23038  xrhmeo  23164  bndth  23176  ismbf3d  23869  dvef  24191  reeff1o  24649  efifo  24742  dvloglem  24842  logf1o2  24844  choc1  28775  shsidmi  28832  shsval2i  28835  omlsii  28851  chdmm1i  28925  chj1i  28937  chm0i  28938  shjshsi  28940  span0  28990  spanuni  28992  sshhococi  28994  spansni  29005  pjoml4i  29035  pjrni  29150  shatomistici  29809  sumdmdlem2  29867  rinvf1o  30014  sigapildsys  30831  sxbrsigalem0  30939  dya2iocucvr  30952  sxbrsigalem4  30955  sxbrsiga  30958  ballotth  31206  kur14lem6  31800  mrsubrn  32017  msubrn  32033  filnetlem3  32971  filnetlem4  32972  onint1  33039  oninhaus  33040  bj-rabtr  33508  bj-rabtrAUTO  33510  bj-disj2r  33593  bj-nuliotaALT  33600  icoreunrn  33809  comptiunov2i  38969  compneOLD  39613  unisnALT  40109  fsumiunss  40729  fourierdlem62  41326  fouriersw  41389  salexct  41490  salgencntex  41499