Theorem eqssi 3999

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

Syntax hints:   = wceq 1542   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  inv1  4395  unv  4396  intab  4983  intabs  5343  intidOLD  5459  dmv  5923  0ima  6078  cnvrescnv  6195  find  7887  findOLD  7888  dftpos4  8230  wfrlem16OLD  8324  dfom3  9642  dmttrcl  9716  rnttrcl  9717  tc2  9737  tcidm  9741  tc0  9742  rankuni  9858  rankval4  9862  djuunxp  9916  djuun  9921  ackbij1  10233  cfom  10259  fin23lem16  10330  itunitc  10416  inaprc  10831  nqerf  10925  dmrecnq  10963  dmaddsr  11080  dmmulsr  11081  axaddf  11140  axmulf  11141  dfnn2  12225  dfuzi  12653  unirnioo  13426  uzrdgfni  13923  0bits  16380  4sqlem19  16896  ledm  18543  lern  18544  efgsfo  19607  0frgp  19647  indiscld  22595  leordtval2  22716  lecldbas  22723  llyidm  22992  nllyidm  22993  toplly  22994  lly1stc  23000  txuni2  23069  txindis  23138  ust0  23724  qdensere  24286  xrtgioo  24322  zdis  24332  xrhmeo  24462  bndth  24474  ismbf3d  25171  dvef  25497  reeff1o  25959  efifo  26056  dvloglem  26156  logf1o2  26158  bday1s  27332  choc1  30580  shsidmi  30637  shsval2i  30640  omlsii  30656  chdmm1i  30730  chj1i  30742  chm0i  30743  shjshsi  30745  span0  30795  spanuni  30797  sshhococi  30799  spansni  30810  pjoml4i  30840  pjrni  30955  shatomistici  31614  sumdmdlem2  31672  rinvf1o  31854  sigapildsys  33160  sxbrsigalem0  33270  dya2iocucvr  33283  sxbrsigalem4  33286  sxbrsiga  33289  ballotth  33536  kur14lem6  34202  mrsubrn  34504  msubrn  34520  filnetlem3  35265  filnetlem4  35266  onint1  35334  oninhaus  35335  bj-rabtr  35810  bj-rabtrAUTO  35812  bj-disj2r  35909  bj-nuliotaALT  35939  bj-idres  36041  icoreunrn  36240  comptiunov2i  42457  unisnALT  43687  fsumiunss  44291  fourierdlem62  44884  fouriersw  44947  salexct  45050  salgencntex  45059