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 709	1 ⊢ 𝐴 = 𝐵

Syntax hints:   = wceq 1541   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930

This theorem is referenced by:  inv1  4359  unv  4360  intab  4944  intabs  5304  intidOLD  5420  dmv  5883  0ima  6035  cnvrescnv  6152  find  7838  findOLD  7839  dftpos4  8181  wfrlem16OLD  8275  dfom3  9592  dmttrcl  9666  rnttrcl  9667  tc2  9687  tcidm  9691  tc0  9692  rankuni  9808  rankval4  9812  djuunxp  9866  djuun  9871  ackbij1  10183  cfom  10209  fin23lem16  10280  itunitc  10366  inaprc  10781  nqerf  10875  dmrecnq  10913  dmaddsr  11030  dmmulsr  11031  axaddf  11090  axmulf  11091  dfnn2  12175  dfuzi  12603  unirnioo  13376  uzrdgfni  13873  0bits  16330  4sqlem19  16846  ledm  18493  lern  18494  efgsfo  19535  0frgp  19575  indiscld  22479  leordtval2  22600  lecldbas  22607  llyidm  22876  nllyidm  22877  toplly  22878  lly1stc  22884  txuni2  22953  txindis  23022  ust0  23608  qdensere  24170  xrtgioo  24206  zdis  24216  xrhmeo  24346  bndth  24358  ismbf3d  25055  dvef  25381  reeff1o  25843  efifo  25940  dvloglem  26040  logf1o2  26042  bday1s  27213  choc1  30332  shsidmi  30389  shsval2i  30392  omlsii  30408  chdmm1i  30482  chj1i  30494  chm0i  30495  shjshsi  30497  span0  30547  spanuni  30549  sshhococi  30551  spansni  30562  pjoml4i  30592  pjrni  30707  shatomistici  31366  sumdmdlem2  31424  rinvf1o  31611  sigapildsys  32850  sxbrsigalem0  32960  dya2iocucvr  32973  sxbrsigalem4  32976  sxbrsiga  32979  ballotth  33226  kur14lem6  33892  mrsubrn  34194  msubrn  34210  filnetlem3  34928  filnetlem4  34929  onint1  34997  oninhaus  34998  bj-rabtr  35473  bj-rabtrAUTO  35475  bj-disj2r  35572  bj-nuliotaALT  35602  bj-idres  35704  icoreunrn  35903  comptiunov2i  42100  unisnALT  43330  fsumiunss  43936  fourierdlem62  44529  fouriersw  44592  salexct  44695  salgencntex  44704