Theorem eqssi 4012

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

Syntax hints:   = wceq 1537   ⊆ wss 3963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-ss 3980

This theorem is referenced by:  inv1  4404  unv  4405  intab  4983  intabs  5355  intidOLD  5469  dmv  5936  0ima  6098  cnvrescnv  6217  find  7918  dftpos4  8269  wfrlem16OLD  8363  dfom3  9685  dmttrcl  9759  rnttrcl  9760  tc2  9780  tcidm  9784  tc0  9785  rankuni  9901  rankval4  9905  djuunxp  9959  djuun  9964  ackbij1  10275  cfom  10302  fin23lem16  10373  itunitc  10459  inaprc  10874  nqerf  10968  dmrecnq  11006  dmaddsr  11123  dmmulsr  11124  axaddf  11183  axmulf  11184  dfnn2  12277  dfuzi  12707  unirnioo  13486  uzrdgfni  13996  0bits  16473  4sqlem19  16997  ledm  18648  lern  18649  efgsfo  19772  0frgp  19812  indiscld  23115  leordtval2  23236  lecldbas  23243  llyidm  23512  nllyidm  23513  toplly  23514  lly1stc  23520  txuni2  23589  txindis  23658  ust0  24244  qdensere  24806  xrtgioo  24842  zdis  24852  xrhmeo  24991  bndth  25004  ismbf3d  25703  dvef  26033  reeff1o  26506  efifo  26604  dvloglem  26705  logf1o2  26707  bday1s  27891  dfn0s2  28351  dfnns2  28377  choc1  31356  shsidmi  31413  shsval2i  31416  omlsii  31432  chdmm1i  31506  chj1i  31518  chm0i  31519  shjshsi  31521  span0  31571  spanuni  31573  sshhococi  31575  spansni  31586  pjoml4i  31616  pjrni  31731  shatomistici  32390  sumdmdlem2  32448  rinvf1o  32647  sigapildsys  34143  sxbrsigalem0  34253  dya2iocucvr  34266  sxbrsigalem4  34269  sxbrsiga  34272  ballotth  34519  kur14lem6  35196  mrsubrn  35498  msubrn  35514  filnetlem3  36363  filnetlem4  36364  onint1  36432  oninhaus  36433  bj-rabtr  36913  bj-rabtrAUTO  36915  bj-disj2r  37011  bj-nuliotaALT  37041  bj-idres  37143  icoreunrn  37342  comptiunov2i  43696  unisnALT  44924  fsumiunss  45531  fourierdlem62  46124  fouriersw  46187  salexct  46290  salgencntex  46299