Theorem eqssi 3948

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

Syntax hints:   = wceq 1541   ⊆ wss 3899

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 2706

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

This theorem is referenced by:  inv1  4348  unv  4349  intab  4931  intabs  5292  dmv  5869  0ima  6035  cnvrescnv  6151  find  7835  dftpos4  8185  dfom3  9554  dmttrcl  9628  rnttrcl  9629  tc2  9647  tcidm  9651  tc0  9652  rankuni  9773  rankval4  9777  djuunxp  9831  djuun  9836  ackbij1  10145  cfom  10172  fin23lem16  10243  itunitc  10329  inaprc  10745  nqerf  10839  dmrecnq  10877  dmaddsr  10994  dmmulsr  10995  axaddf  11054  axmulf  11055  dfnn2  12156  dfuzi  12581  unirnioo  13363  uzrdgfni  13879  0bits  16364  4sqlem19  16889  ledm  18511  lern  18512  efgsfo  19666  0frgp  19706  indiscld  23033  leordtval2  23154  lecldbas  23161  llyidm  23430  nllyidm  23431  toplly  23432  lly1stc  23438  txuni2  23507  txindis  23576  ust0  24162  qdensere  24711  xrtgioo  24749  zdis  24759  xrhmeo  24898  bndth  24911  ismbf3d  25609  dvef  25938  reeff1o  26411  efifo  26510  dvloglem  26611  logf1o2  26613  bday1s  27802  onsiso  28236  dfn0s2  28292  bdayn0sf1o  28328  dfnns2  28330  choc1  31351  shsidmi  31408  shsval2i  31411  omlsii  31427  chdmm1i  31501  chj1i  31513  chm0i  31514  shjshsi  31516  span0  31566  spanuni  31568  sshhococi  31570  spansni  31581  pjoml4i  31611  pjrni  31726  shatomistici  32385  sumdmdlem2  32443  rinvf1o  32657  sigapildsys  34268  sxbrsigalem0  34377  dya2iocucvr  34390  sxbrsigalem4  34393  sxbrsiga  34396  ballotth  34644  kur14lem6  35354  mrsubrn  35656  msubrn  35672  filnetlem3  36523  filnetlem4  36524  onint1  36592  oninhaus  36593  bj-rabtr  37074  bj-rabtrAUTO  37076  bj-disj2r  37172  bj-nuliotaALT  37202  bj-idres  37304  icoreunrn  37503  dmsucmap  38581  comptiunov2i  43889  unisnALT  45108  fsumiunss  45763  fourierdlem62  46354  fouriersw  46417  salexct  46520  salgencntex  46529