Theorem eqssi 3931

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

Syntax hints:   = wceq 1547   ⊆ wss 3883

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 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-ss 3900

This theorem is referenced by:  inv1  4326  unv  4327  intab  4908  intabs  5277  dmv  5864  0ima  6030  cnvrescnv  6146  find  7835  dftpos4  8185  dfom3  9559  dmttrcl  9633  rnttrcl  9634  tc2  9652  tcidm  9656  tc0  9657  rankuni  9778  rankval4  9782  djuunxp  9836  djuun  9841  ackbij1  10150  cfom  10177  fin23lem16  10248  itunitc  10334  inaprc  10750  nqerf  10844  dmrecnq  10882  dmaddsr  10999  dmmulsr  11000  axaddf  11059  axmulf  11060  dfnn2  12178  dfuzi  12611  unirnioo  13393  uzrdgfni  13911  0bits  16399  4sqlem19  16925  ledm  18547  lern  18548  efgsfo  19705  0frgp  19745  indiscld  23074  leordtval2  23195  lecldbas  23202  llyidm  23471  nllyidm  23472  toplly  23473  lly1stc  23479  txuni2  23548  txindis  23617  ust0  24203  qdensere  24752  xrtgioo  24790  zdis  24800  xrhmeo  24931  bndth  24943  ismbf3d  25639  dvef  25965  reeff1o  26430  efifo  26529  dvloglem  26630  logf1o2  26632  bday1  27824  oniso  28281  dfn0s2  28342  bdayn0sf1o  28380  dfnns2  28382  choc1  31416  shsidmi  31473  shsval2i  31476  omlsii  31492  chdmm1i  31566  chj1i  31578  chm0i  31579  shjshsi  31581  span0  31631  spanuni  31633  sshhococi  31635  spansni  31646  pjoml4i  31676  pjrni  31791  shatomistici  32450  sumdmdlem2  32508  rinvf1o  32722  sigapildsys  34346  sxbrsigalem0  34455  dya2iocucvr  34468  sxbrsigalem4  34471  sxbrsiga  34474  ballotth  34722  kur14lem6  35439  mrsubrn  35741  msubrn  35757  filnetlem3  36608  filnetlem4  36609  onint1  36677  oninhaus  36678  ttcuniun  36738  ttciunun  36739  ttcuni  36741  dfttc4  36758  bj-rabtr  37283  bj-rabtrAUTO  37285  bj-disj2r  37381  bj-nuliotaALT  37411  bj-idres  37520  icoreunrn  37721  dmsucmap  38835  comptiunov2i  44150  unisnALT  45369  fsumiunss  46020  fourierdlem62  46611  fouriersw  46674  salexct  46777  salgencntex  46786