Theorem eqssi 3961

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

Syntax hints:   = wceq 1567   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ss 3930

This theorem is referenced by:  inv1  4362  unv  4363  intab  4947  intabs  5320  dmv  5913  0ima  6081  cnvrescnv  6195  find  7892  dftpos4  8241  dfom3  9616  dmttrcl  9690  rnttrcl  9691  tc2  9709  tcidm  9713  tc0  9714  rankuni  9835  rankval4  9839  djuunxp  9907  djuun  9912  ackbij1  10220  cfom  10248  fin23lem16  10319  itunitc  10405  inaprc  10821  nqerf  10915  dmrecnq  10953  dmaddsr  11070  dmmulsr  11071  axaddf  11130  axmulf  11131  dfnn2  12246  dfuzi  12687  unirnioo  13476  uzrdgfni  13994  sgnrn  15135  0bits  16497  4sqlem19  17023  ledm  18646  lern  18647  efgsfo  19809  0frgp  19849  indiscld  23217  leordtval2  23338  lecldbas  23345  llyidm  23614  nllyidm  23615  toplly  23616  lly1stc  23622  txuni2  23691  txindis  23760  ust0  24346  qdensere  24895  xrtgioo  24933  zdis  24943  xrhmeo  25074  bndth  25086  ismbf3d  25782  dvef  26108  reeff1o  26576  efifo  26678  dvloglem  26779  logf1o2  26781  bday1  27973  oniso  28430  dfn0s2  28491  bdayn0sf1o  28529  dfnns2  28531  choc1  31620  shsidmi  31677  shsval2i  31680  omlsii  31696  chdmm1i  31770  chj1i  31782  chm0i  31783  shjshsi  31785  span0  31835  spanuni  31837  sshhococi  31839  spansni  31850  pjoml4i  31880  pjrni  31995  shatomistici  32654  sumdmdlem2  32712  rinvf1o  32916  sigapildsys  34497  sxbrsigalem0  34606  dya2iocucvr  34619  sxbrsigalem4  34622  sxbrsiga  34625  ballotth  34873  kur14lem6  35602  mrsubrn  35904  msubrn  35920  filnetlem3  36780  filnetlem4  36781  onint1  36849  oninhaus  36850  ttcuniun  36910  ttciunun  36911  ttcuni  36913  dfttc4  36930  bj-rabtr  37454  bj-rabtrAUTO  37456  bj-disj2r  37552  bj-nuliotaALT  37582  bj-idres  37692  icoreunrn  37893  dmsucmap  39007  comptiunov2i  44324  unisnALT  45526  fsumiunss  46183  fourierdlem62  46774  fouriersw  46837  salexct  46940  salgencntex  46949