Theorem eqssi 3928

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

This proof depends on syntax axioms:   = wceq 1569   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2755  df-ss 3900

This theorem is used by:  inv1  4350  unv  4351  intab  4940  intabs  5313  dmv  5908  cnvrescnv  6193  0ima  6206  find  7914  dftpos4  8273  dfom3  9658  dmttrcl  9732  rnttrcl  9733  tc2  9751  tcidm  9755  tc0  9756  rankuni  9889  rankval4  9894  djuunxp  10012  djuun  10017  ackbij1  10325  cfom  10352  fin23lem16  10423  itunitc  10509  inaprc  10931  nqerf  11025  dmrecnq  11063  dmaddsr  11180  dmmulsr  11181  axaddf  11240  axmulf  11241  dfnn2  12358  dfuzi  12800  unirnioo  13590  uzrdgfni  14111  sgnrn  15263  0bits  16621  4sqlem19  17153  ledm  18776  lern  18777  efgsfo  19965  0frgp  20005  indiscld  23421  leordtval2  23542  lecldbas  23549  llyidm  23819  nllyidm  23820  toplly  23821  lly1stc  23827  txuni2  23896  txindis  23965  ust0  24551  qdensere  25100  xrtgioo  25138  zdis  25148  xrhmeo  25279  bndth  25291  ismbf3d  25987  dvef  26312  reeff1o  26786  efifo  26887  dvloglem  26988  logf1o2  26990  bday1  28212  oniso  28669  dfn0s2  28730  bdayn0sf1o  28768  dfnns2  28770  choc1  31941  shsidmi  31998  shsval2i  32001  omlsii  32017  chdmm1i  32091  chj1i  32103  chm0i  32104  shjshsi  32106  span0  32156  spanuni  32158  sshhococi  32160  spansni  32171  pjoml4i  32201  pjrni  32316  shatomistici  32975  sumdmdlem2  33033  rinvf1o  33278  sigapildsys  34848  sxbrsigalem0  34956  dya2iocucvr  34969  sxbrsigalem4  34972  sxbrsiga  34975  ballotth  35223  scottidm  35820  jf1o  35965  kur14lem6  36097  mrsubrn  36399  msubrn  36415  filnetlem3  37295  filnetlem4  37296  onint1  37364  oninhaus  37365  ttcuniun  37425  ttciunun  37426  ttcuni  37428  dfttc4  37445  bj-rabtr  37970  bj-rabtrAUTO  37972  bj-disj2r  38068  bj-nuliotaALT  38112  bj-idres  38221  icoreunrn  38422  dfprop  38787  dmsucmap  39540  comptiunov2i  44846  unisnALT  46047  fsumiunss  46726  fourierdlem62  47317  fouriersw  47380  salexct  47483  salgencntex  47492