Theorem eqssi 3946

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

Syntax hints:   = wceq 1541   ⊆ wss 3897

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 2121  ax-ext 2703

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

This theorem is referenced by:  inv1  4345  unv  4346  intab  4926  intabs  5285  dmv  5861  0ima  6026  cnvrescnv  6142  find  7825  dftpos4  8175  dfom3  9537  dmttrcl  9611  rnttrcl  9612  tc2  9630  tcidm  9634  tc0  9635  rankuni  9756  rankval4  9760  djuunxp  9814  djuun  9819  ackbij1  10128  cfom  10155  fin23lem16  10226  itunitc  10312  inaprc  10727  nqerf  10821  dmrecnq  10859  dmaddsr  10976  dmmulsr  10977  axaddf  11036  axmulf  11037  dfnn2  12138  dfuzi  12564  unirnioo  13349  uzrdgfni  13865  0bits  16350  4sqlem19  16875  ledm  18496  lern  18497  efgsfo  19651  0frgp  19691  indiscld  23006  leordtval2  23127  lecldbas  23134  llyidm  23403  nllyidm  23404  toplly  23405  lly1stc  23411  txuni2  23480  txindis  23549  ust0  24135  qdensere  24684  xrtgioo  24722  zdis  24732  xrhmeo  24871  bndth  24884  ismbf3d  25582  dvef  25911  reeff1o  26384  efifo  26483  dvloglem  26584  logf1o2  26586  bday1s  27775  onsiso  28205  dfn0s2  28260  bdayn0sf1o  28295  dfnns2  28297  choc1  31307  shsidmi  31364  shsval2i  31367  omlsii  31383  chdmm1i  31457  chj1i  31469  chm0i  31470  shjshsi  31472  span0  31522  spanuni  31524  sshhococi  31526  spansni  31537  pjoml4i  31567  pjrni  31682  shatomistici  32341  sumdmdlem2  32399  rinvf1o  32612  sigapildsys  34175  sxbrsigalem0  34284  dya2iocucvr  34297  sxbrsigalem4  34300  sxbrsiga  34303  ballotth  34551  kur14lem6  35255  mrsubrn  35557  msubrn  35573  filnetlem3  36424  filnetlem4  36425  onint1  36493  oninhaus  36494  bj-rabtr  36974  bj-rabtrAUTO  36976  bj-disj2r  37072  bj-nuliotaALT  37102  bj-idres  37204  icoreunrn  37403  dmsucmap  38491  comptiunov2i  43809  unisnALT  45028  fsumiunss  45685  fourierdlem62  46276  fouriersw  46339  salexct  46442  salgencntex  46451