Theorem eqssi 3954

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

This proof depends on syntax axioms:   = wceq 1570   ⊆ wss 3906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-ss 3923

This theorem is used by:  inv1  4355  unv  4356  intab  4945  intabs  5321  dmv  5914  0ima  6082  cnvrescnv  6196  find  7898  dftpos4  8247  dfom3  9623  dmttrcl  9697  rnttrcl  9698  tc2  9716  tcidm  9720  tc0  9721  rankuni  9842  rankval4  9846  djuunxp  9923  djuun  9928  ackbij1  10236  cfom  10263  fin23lem16  10334  itunitc  10420  inaprc  10838  nqerf  10932  dmrecnq  10970  dmaddsr  11087  dmmulsr  11088  axaddf  11147  axmulf  11148  dfnn2  12263  dfuzi  12705  unirnioo  13494  uzrdgfni  14014  sgnrn  15161  0bits  16521  4sqlem19  17047  ledm  18670  lern  18671  efgsfo  19855  0frgp  19895  indiscld  23300  leordtval2  23421  lecldbas  23428  llyidm  23698  nllyidm  23699  toplly  23700  lly1stc  23706  txuni2  23775  txindis  23844  ust0  24430  qdensere  24979  xrtgioo  25017  zdis  25027  xrhmeo  25158  bndth  25170  ismbf3d  25866  dvef  26192  reeff1o  26663  efifo  26765  dvloglem  26866  logf1o2  26868  bday1  28060  oniso  28517  dfn0s2  28578  bdayn0sf1o  28616  dfnns2  28618  choc1  31752  shsidmi  31809  shsval2i  31812  omlsii  31828  chdmm1i  31902  chj1i  31914  chm0i  31915  shjshsi  31917  span0  31967  spanuni  31969  sshhococi  31971  spansni  31982  pjoml4i  32012  pjrni  32127  shatomistici  32786  sumdmdlem2  32844  rinvf1o  33048  sigapildsys  34619  sxbrsigalem0  34728  dya2iocucvr  34741  sxbrsigalem4  34744  sxbrsiga  34747  ballotth  34995  kur14lem6  35742  mrsubrn  36044  msubrn  36060  filnetlem3  36950  filnetlem4  36951  onint1  37019  oninhaus  37020  ttcuniun  37080  ttciunun  37081  ttcuni  37083  dfttc4  37100  bj-rabtr  37625  bj-rabtrAUTO  37627  bj-disj2r  37723  bj-nuliotaALT  37753  bj-idres  37863  icoreunrn  38064  dmsucmap  39177  comptiunov2i  44492  unisnALT  45694  fsumiunss  46351  fourierdlem62  46942  fouriersw  47005  salexct  47108  salgencntex  47117