Theorem eqssi 3963

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

Syntax hints:   = wceq 1540   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3931

This theorem is referenced by:  inv1  4361  unv  4362  intab  4942  intabs  5304  intidOLD  5418  dmv  5886  0ima  6049  cnvrescnv  6168  find  7871  dftpos4  8224  dfom3  9600  dmttrcl  9674  rnttrcl  9675  tc2  9695  tcidm  9699  tc0  9700  rankuni  9816  rankval4  9820  djuunxp  9874  djuun  9879  ackbij1  10190  cfom  10217  fin23lem16  10288  itunitc  10374  inaprc  10789  nqerf  10883  dmrecnq  10921  dmaddsr  11038  dmmulsr  11039  axaddf  11098  axmulf  11099  dfnn2  12199  dfuzi  12625  unirnioo  13410  uzrdgfni  13923  0bits  16409  4sqlem19  16934  ledm  18549  lern  18550  efgsfo  19669  0frgp  19709  indiscld  22978  leordtval2  23099  lecldbas  23106  llyidm  23375  nllyidm  23376  toplly  23377  lly1stc  23383  txuni2  23452  txindis  23521  ust0  24107  qdensere  24657  xrtgioo  24695  zdis  24705  xrhmeo  24844  bndth  24857  ismbf3d  25555  dvef  25884  reeff1o  26357  efifo  26456  dvloglem  26557  logf1o2  26559  bday1s  27743  onsiso  28169  dfn0s2  28224  bdayn0sf1o  28259  dfnns2  28261  choc1  31256  shsidmi  31313  shsval2i  31316  omlsii  31332  chdmm1i  31406  chj1i  31418  chm0i  31419  shjshsi  31421  span0  31471  spanuni  31473  sshhococi  31475  spansni  31486  pjoml4i  31516  pjrni  31631  shatomistici  32290  sumdmdlem2  32348  rinvf1o  32554  sigapildsys  34152  sxbrsigalem0  34262  dya2iocucvr  34275  sxbrsigalem4  34278  sxbrsiga  34281  ballotth  34529  kur14lem6  35198  mrsubrn  35500  msubrn  35516  filnetlem3  36368  filnetlem4  36369  onint1  36437  oninhaus  36438  bj-rabtr  36918  bj-rabtrAUTO  36920  bj-disj2r  37016  bj-nuliotaALT  37046  bj-idres  37148  icoreunrn  37347  comptiunov2i  43695  unisnALT  44915  fsumiunss  45573  fourierdlem62  46166  fouriersw  46229  salexct  46332  salgencntex  46341