Theorem eqssi 3939

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

Syntax hints:   = wceq 1537   ⊆ wss 3889

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-8 2103  ax-9 2111  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1540  df-ex 1778  df-sb 2063  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3436  df-in 3896  df-ss 3906

This theorem is referenced by:  inv1  4331  unv  4332  intab  4912  intabs  5269  intid  5376  dmv  5835  0ima  5987  cnvrescnv  6102  find  7763  findOLD  7764  dftpos4  8081  wfrlem16OLD  8175  dfom3  9433  dmttrcl  9507  rnttrcl  9508  tc2  9528  tcidm  9532  tc0  9533  rankuni  9649  rankval4  9653  djuunxp  9707  djuun  9712  ackbij1  10022  cfom  10048  fin23lem16  10119  itunitc  10205  inaprc  10620  nqerf  10714  dmrecnq  10752  dmaddsr  10869  dmmulsr  10870  axaddf  10929  axmulf  10930  dfnn2  12014  dfuzi  12439  unirnioo  13209  uzrdgfni  13706  0bits  16174  4sqlem19  16692  ledm  18336  lern  18337  efgsfo  19373  0frgp  19413  indiscld  22270  leordtval2  22391  lecldbas  22398  llyidm  22667  nllyidm  22668  toplly  22669  lly1stc  22675  txuni2  22744  txindis  22813  ust0  23399  qdensere  23961  xrtgioo  23997  zdis  24007  xrhmeo  24137  bndth  24149  ismbf3d  24846  dvef  25172  reeff1o  25634  efifo  25731  dvloglem  25831  logf1o2  25833  choc1  29717  shsidmi  29774  shsval2i  29777  omlsii  29793  chdmm1i  29867  chj1i  29879  chm0i  29880  shjshsi  29882  span0  29932  spanuni  29934  sshhococi  29936  spansni  29947  pjoml4i  29977  pjrni  30092  shatomistici  30751  sumdmdlem2  30809  rinvf1o  30993  sigapildsys  32158  sxbrsigalem0  32266  dya2iocucvr  32279  sxbrsigalem4  32282  sxbrsiga  32285  ballotth  32532  kur14lem6  33201  mrsubrn  33503  msubrn  33519  bday1s  34053  filnetlem3  34597  filnetlem4  34598  onint1  34666  oninhaus  34667  bj-rabtr  35146  bj-rabtrAUTO  35148  bj-disj2r  35246  bj-nuliotaALT  35257  bj-idres  35359  icoreunrn  35558  comptiunov2i  41338  unisnALT  42570  fsumiunss  43151  fourierdlem62  43744  fouriersw  43807  salexct  43908  salgencntex  43917