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 710	1 ⊢ 𝐴 = 𝐵

Syntax hints:   = wceq 1538   ⊆ wss 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  inv1  4302  unv  4303  intab  4868  intabs  5209  intid  5315  dmv  5756  0ima  5913  cnvrescnv  6019  find  7587  findOLD  7588  dftpos4  7894  wfrlem16  7953  dfom3  9094  tc2  9168  tcidm  9172  tc0  9173  rankuni  9276  rankval4  9280  djuunxp  9334  djuun  9339  ackbij1  9649  cfom  9675  fin23lem16  9746  itunitc  9832  inaprc  10247  nqerf  10341  dmrecnq  10379  dmaddsr  10496  dmmulsr  10497  axaddf  10556  axmulf  10557  dfnn2  11638  dfuzi  12061  unirnioo  12827  uzrdgfni  13321  0bits  15778  4sqlem19  16289  ledm  17826  lern  17827  efgsfo  18857  0frgp  18897  indiscld  21696  leordtval2  21817  lecldbas  21824  llyidm  22093  nllyidm  22094  toplly  22095  lly1stc  22101  txuni2  22170  txindis  22239  ust0  22825  qdensere  23375  xrtgioo  23411  zdis  23421  xrhmeo  23551  bndth  23563  ismbf3d  24258  dvef  24583  reeff1o  25042  efifo  25139  dvloglem  25239  logf1o2  25241  choc1  29110  shsidmi  29167  shsval2i  29170  omlsii  29186  chdmm1i  29260  chj1i  29272  chm0i  29273  shjshsi  29275  span0  29325  spanuni  29327  sshhococi  29329  spansni  29340  pjoml4i  29370  pjrni  29485  shatomistici  30144  sumdmdlem2  30202  rinvf1o  30389  sigapildsys  31531  sxbrsigalem0  31639  dya2iocucvr  31652  sxbrsigalem4  31655  sxbrsiga  31658  ballotth  31905  kur14lem6  32571  mrsubrn  32873  msubrn  32889  filnetlem3  33841  filnetlem4  33842  onint1  33910  oninhaus  33911  bj-rabtr  34372  bj-rabtrAUTO  34374  bj-disj2r  34464  bj-nuliotaALT  34475  bj-idres  34575  icoreunrn  34776  comptiunov2i  40407  unisnALT  41632  fsumiunss  42217  fourierdlem62  42810  fouriersw  42873  salexct  42974  salgencntex  42983