Theorem eqssi 3950

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

Syntax hints:   = wceq 1541   ⊆ wss 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ss 3918

This theorem is referenced by:  inv1  4350  unv  4351  intab  4933  intabs  5294  dmv  5871  0ima  6037  cnvrescnv  6153  find  7837  dftpos4  8187  dfom3  9556  dmttrcl  9630  rnttrcl  9631  tc2  9649  tcidm  9653  tc0  9654  rankuni  9775  rankval4  9779  djuunxp  9833  djuun  9838  ackbij1  10147  cfom  10174  fin23lem16  10245  itunitc  10331  inaprc  10747  nqerf  10841  dmrecnq  10879  dmaddsr  10996  dmmulsr  10997  axaddf  11056  axmulf  11057  dfnn2  12158  dfuzi  12583  unirnioo  13365  uzrdgfni  13881  0bits  16366  4sqlem19  16891  ledm  18513  lern  18514  efgsfo  19668  0frgp  19708  indiscld  23035  leordtval2  23156  lecldbas  23163  llyidm  23432  nllyidm  23433  toplly  23434  lly1stc  23440  txuni2  23509  txindis  23578  ust0  24164  qdensere  24713  xrtgioo  24751  zdis  24761  xrhmeo  24900  bndth  24913  ismbf3d  25611  dvef  25940  reeff1o  26413  efifo  26512  dvloglem  26613  logf1o2  26615  bday1  27810  oniso  28267  dfn0s2  28328  bdayn0sf1o  28366  dfnns2  28368  choc1  31402  shsidmi  31459  shsval2i  31462  omlsii  31478  chdmm1i  31552  chj1i  31564  chm0i  31565  shjshsi  31567  span0  31617  spanuni  31619  sshhococi  31621  spansni  31632  pjoml4i  31662  pjrni  31777  shatomistici  32436  sumdmdlem2  32494  rinvf1o  32708  sigapildsys  34319  sxbrsigalem0  34428  dya2iocucvr  34441  sxbrsigalem4  34444  sxbrsiga  34447  ballotth  34695  kur14lem6  35405  mrsubrn  35707  msubrn  35723  filnetlem3  36574  filnetlem4  36575  onint1  36643  oninhaus  36644  bj-rabtr  37131  bj-rabtrAUTO  37133  bj-disj2r  37229  bj-nuliotaALT  37259  bj-idres  37365  icoreunrn  37564  dmsucmap  38652  comptiunov2i  43957  unisnALT  45176  fsumiunss  45831  fourierdlem62  46422  fouriersw  46485  salexct  46588  salgencntex  46597