Theorem eqssi 3996

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

Syntax hints:   = wceq 1534   ⊆ wss 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2718  df-ss 3964

This theorem is referenced by:  inv1  4399  unv  4400  intab  4988  intabs  5351  intidOLD  5466  dmv  5931  0ima  6089  cnvrescnv  6208  find  7910  dftpos4  8262  wfrlem16OLD  8356  dfom3  9692  dmttrcl  9766  rnttrcl  9767  tc2  9787  tcidm  9791  tc0  9792  rankuni  9908  rankval4  9912  djuunxp  9966  djuun  9971  ackbij1  10283  cfom  10309  fin23lem16  10380  itunitc  10466  inaprc  10881  nqerf  10975  dmrecnq  11013  dmaddsr  11130  dmmulsr  11131  axaddf  11190  axmulf  11191  dfnn2  12279  dfuzi  12707  unirnioo  13482  uzrdgfni  13980  0bits  16441  4sqlem19  16967  ledm  18617  lern  18618  efgsfo  19739  0frgp  19779  indiscld  23089  leordtval2  23210  lecldbas  23217  llyidm  23486  nllyidm  23487  toplly  23488  lly1stc  23494  txuni2  23563  txindis  23632  ust0  24218  qdensere  24780  xrtgioo  24816  zdis  24826  xrhmeo  24965  bndth  24978  ismbf3d  25677  dvef  26006  reeff1o  26480  efifo  26577  dvloglem  26678  logf1o2  26680  bday1s  27864  dfn0s2  28307  choc1  31263  shsidmi  31320  shsval2i  31323  omlsii  31339  chdmm1i  31413  chj1i  31425  chm0i  31426  shjshsi  31428  span0  31478  spanuni  31480  sshhococi  31482  spansni  31493  pjoml4i  31523  pjrni  31638  shatomistici  32297  sumdmdlem2  32355  rinvf1o  32549  sigapildsys  33997  sxbrsigalem0  34107  dya2iocucvr  34120  sxbrsigalem4  34123  sxbrsiga  34126  ballotth  34373  kur14lem6  35041  mrsubrn  35343  msubrn  35359  filnetlem3  36094  filnetlem4  36095  onint1  36163  oninhaus  36164  bj-rabtr  36638  bj-rabtrAUTO  36640  bj-disj2r  36737  bj-nuliotaALT  36767  bj-idres  36869  icoreunrn  37068  comptiunov2i  43391  unisnALT  44620  fsumiunss  45214  fourierdlem62  45807  fouriersw  45870  salexct  45973  salgencntex  45982