Theorem eqssi 3933

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

Syntax hints:   = wceq 1539   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  inv1  4325  unv  4326  intab  4906  intabs  5261  intid  5367  dmv  5820  0ima  5975  cnvrescnv  6087  find  7717  findOLD  7718  dftpos4  8032  wfrlem16OLD  8126  dfom3  9335  tc2  9431  tcidm  9435  tc0  9436  rankuni  9552  rankval4  9556  djuunxp  9610  djuun  9615  ackbij1  9925  cfom  9951  fin23lem16  10022  itunitc  10108  inaprc  10523  nqerf  10617  dmrecnq  10655  dmaddsr  10772  dmmulsr  10773  axaddf  10832  axmulf  10833  dfnn2  11916  dfuzi  12341  unirnioo  13110  uzrdgfni  13606  0bits  16074  4sqlem19  16592  ledm  18223  lern  18224  efgsfo  19260  0frgp  19300  indiscld  22150  leordtval2  22271  lecldbas  22278  llyidm  22547  nllyidm  22548  toplly  22549  lly1stc  22555  txuni2  22624  txindis  22693  ust0  23279  qdensere  23839  xrtgioo  23875  zdis  23885  xrhmeo  24015  bndth  24027  ismbf3d  24723  dvef  25049  reeff1o  25511  efifo  25608  dvloglem  25708  logf1o2  25710  choc1  29590  shsidmi  29647  shsval2i  29650  omlsii  29666  chdmm1i  29740  chj1i  29752  chm0i  29753  shjshsi  29755  span0  29805  spanuni  29807  sshhococi  29809  spansni  29820  pjoml4i  29850  pjrni  29965  shatomistici  30624  sumdmdlem2  30682  rinvf1o  30866  sigapildsys  32030  sxbrsigalem0  32138  dya2iocucvr  32151  sxbrsigalem4  32154  sxbrsiga  32157  ballotth  32404  kur14lem6  33073  mrsubrn  33375  msubrn  33391  dmttrcl  33707  rnttrcl  33708  bday1s  33952  filnetlem3  34496  filnetlem4  34497  onint1  34565  oninhaus  34566  bj-rabtr  35045  bj-rabtrAUTO  35047  bj-disj2r  35145  bj-nuliotaALT  35156  bj-idres  35258  icoreunrn  35457  comptiunov2i  41203  unisnALT  42435  fsumiunss  43006  fourierdlem62  43599  fouriersw  43662  salexct  43763  salgencntex  43772