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

Syntax hints:   = wceq 1539   ⊆ wss 3950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2728  df-ss 3967

This theorem is referenced by:  inv1  4397  unv  4398  intab  4977  intabs  5348  intidOLD  5462  dmv  5932  0ima  6095  cnvrescnv  6214  find  7918  dftpos4  8271  wfrlem16OLD  8365  dfom3  9688  dmttrcl  9762  rnttrcl  9763  tc2  9783  tcidm  9787  tc0  9788  rankuni  9904  rankval4  9908  djuunxp  9962  djuun  9967  ackbij1  10278  cfom  10305  fin23lem16  10376  itunitc  10462  inaprc  10877  nqerf  10971  dmrecnq  11009  dmaddsr  11126  dmmulsr  11127  axaddf  11186  axmulf  11187  dfnn2  12280  dfuzi  12711  unirnioo  13490  uzrdgfni  14000  0bits  16477  4sqlem19  17002  ledm  18636  lern  18637  efgsfo  19758  0frgp  19798  indiscld  23100  leordtval2  23221  lecldbas  23228  llyidm  23497  nllyidm  23498  toplly  23499  lly1stc  23505  txuni2  23574  txindis  23643  ust0  24229  qdensere  24791  xrtgioo  24829  zdis  24839  xrhmeo  24978  bndth  24991  ismbf3d  25690  dvef  26019  reeff1o  26492  efifo  26590  dvloglem  26691  logf1o2  26693  bday1s  27877  dfn0s2  28337  dfnns2  28363  choc1  31347  shsidmi  31404  shsval2i  31407  omlsii  31423  chdmm1i  31497  chj1i  31509  chm0i  31510  shjshsi  31512  span0  31562  spanuni  31564  sshhococi  31566  spansni  31577  pjoml4i  31607  pjrni  31722  shatomistici  32381  sumdmdlem2  32439  rinvf1o  32641  sigapildsys  34164  sxbrsigalem0  34274  dya2iocucvr  34287  sxbrsigalem4  34290  sxbrsiga  34293  ballotth  34541  kur14lem6  35217  mrsubrn  35519  msubrn  35535  filnetlem3  36382  filnetlem4  36383  onint1  36451  oninhaus  36452  bj-rabtr  36932  bj-rabtrAUTO  36934  bj-disj2r  37030  bj-nuliotaALT  37060  bj-idres  37162  icoreunrn  37361  comptiunov2i  43724  unisnALT  44951  fsumiunss  45595  fourierdlem62  46188  fouriersw  46251  salexct  46354  salgencntex  46363