Theorem eqssi 3947

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

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

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 2155  ax-ext 2732

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

This theorem is used by:  inv1  4348  unv  4349  intab  4938  intabs  5313  dmv  5906  0ima  6074  cnvrescnv  6189  find  7893  dftpos4  8244  dfom3  9629  dmttrcl  9703  rnttrcl  9704  tc2  9722  tcidm  9726  tc0  9727  rankuni  9848  rankval4  9852  djuunxp  9929  djuun  9934  ackbij1  10242  cfom  10269  fin23lem16  10340  itunitc  10426  inaprc  10848  nqerf  10942  dmrecnq  10980  dmaddsr  11097  dmmulsr  11098  axaddf  11157  axmulf  11158  dfnn2  12273  dfuzi  12715  unirnioo  13505  uzrdgfni  14025  sgnrn  15174  0bits  16532  4sqlem19  17058  ledm  18681  lern  18682  efgsfo  19869  0frgp  19909  indiscld  23319  leordtval2  23440  lecldbas  23447  llyidm  23717  nllyidm  23718  toplly  23719  lly1stc  23725  txuni2  23794  txindis  23863  ust0  24449  qdensere  24998  xrtgioo  25036  zdis  25046  xrhmeo  25177  bndth  25189  ismbf3d  25885  dvef  26210  reeff1o  26686  efifo  26787  dvloglem  26888  logf1o2  26890  bday1  28082  oniso  28539  dfn0s2  28600  bdayn0sf1o  28638  dfnns2  28640  choc1  31811  shsidmi  31868  shsval2i  31871  omlsii  31887  chdmm1i  31961  chj1i  31973  chm0i  31974  shjshsi  31976  span0  32026  spanuni  32028  sshhococi  32030  spansni  32041  pjoml4i  32071  pjrni  32186  shatomistici  32845  sumdmdlem2  32903  rinvf1o  33106  sigapildsys  34676  sxbrsigalem0  34785  dya2iocucvr  34798  sxbrsigalem4  34801  sxbrsiga  34804  ballotth  35052  kur14lem6  35793  mrsubrn  36095  msubrn  36111  filnetlem3  37002  filnetlem4  37003  onint1  37071  oninhaus  37072  ttcuniun  37132  ttciunun  37133  ttcuni  37135  dfttc4  37152  bj-rabtr  37677  bj-rabtrAUTO  37679  bj-disj2r  37775  bj-nuliotaALT  37805  bj-idres  37915  icoreunrn  38116  dmsucmap  39219  comptiunov2i  44549  unisnALT  45751  fsumiunss  46408  fourierdlem62  46999  fouriersw  47062  salexct  47165  salgencntex  47174