Theorem eqssi 4025

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

Syntax hints:   = wceq 1537   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993

This theorem is referenced by:  inv1  4421  unv  4422  intab  5002  intabs  5367  intidOLD  5478  dmv  5947  0ima  6107  cnvrescnv  6226  find  7935  dftpos4  8286  wfrlem16OLD  8380  dfom3  9716  dmttrcl  9790  rnttrcl  9791  tc2  9811  tcidm  9815  tc0  9816  rankuni  9932  rankval4  9936  djuunxp  9990  djuun  9995  ackbij1  10306  cfom  10333  fin23lem16  10404  itunitc  10490  inaprc  10905  nqerf  10999  dmrecnq  11037  dmaddsr  11154  dmmulsr  11155  axaddf  11214  axmulf  11215  dfnn2  12306  dfuzi  12734  unirnioo  13509  uzrdgfni  14009  0bits  16485  4sqlem19  17010  ledm  18660  lern  18661  efgsfo  19781  0frgp  19821  indiscld  23120  leordtval2  23241  lecldbas  23248  llyidm  23517  nllyidm  23518  toplly  23519  lly1stc  23525  txuni2  23594  txindis  23663  ust0  24249  qdensere  24811  xrtgioo  24847  zdis  24857  xrhmeo  24996  bndth  25009  ismbf3d  25708  dvef  26038  reeff1o  26509  efifo  26607  dvloglem  26708  logf1o2  26710  bday1s  27894  dfn0s2  28354  dfnns2  28380  choc1  31359  shsidmi  31416  shsval2i  31419  omlsii  31435  chdmm1i  31509  chj1i  31521  chm0i  31522  shjshsi  31524  span0  31574  spanuni  31576  sshhococi  31578  spansni  31589  pjoml4i  31619  pjrni  31734  shatomistici  32393  sumdmdlem2  32451  rinvf1o  32649  sigapildsys  34126  sxbrsigalem0  34236  dya2iocucvr  34249  sxbrsigalem4  34252  sxbrsiga  34255  ballotth  34502  kur14lem6  35179  mrsubrn  35481  msubrn  35497  filnetlem3  36346  filnetlem4  36347  onint1  36415  oninhaus  36416  bj-rabtr  36896  bj-rabtrAUTO  36898  bj-disj2r  36994  bj-nuliotaALT  37024  bj-idres  37126  icoreunrn  37325  comptiunov2i  43668  unisnALT  44897  fsumiunss  45496  fourierdlem62  46089  fouriersw  46152  salexct  46255  salgencntex  46264