Theorem eqssi 3952

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

Syntax hints:   = wceq 1542   ⊆ wss 3903

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3920

This theorem is referenced by:  inv1  4352  unv  4353  intab  4935  intabs  5296  dmv  5879  0ima  6045  cnvrescnv  6161  find  7847  dftpos4  8197  dfom3  9568  dmttrcl  9642  rnttrcl  9643  tc2  9661  tcidm  9665  tc0  9666  rankuni  9787  rankval4  9791  djuunxp  9845  djuun  9850  ackbij1  10159  cfom  10186  fin23lem16  10257  itunitc  10343  inaprc  10759  nqerf  10853  dmrecnq  10891  dmaddsr  11008  dmmulsr  11009  axaddf  11068  axmulf  11069  dfnn2  12170  dfuzi  12595  unirnioo  13377  uzrdgfni  13893  0bits  16378  4sqlem19  16903  ledm  18525  lern  18526  efgsfo  19683  0frgp  19723  indiscld  23050  leordtval2  23171  lecldbas  23178  llyidm  23447  nllyidm  23448  toplly  23449  lly1stc  23455  txuni2  23524  txindis  23593  ust0  24179  qdensere  24728  xrtgioo  24766  zdis  24776  xrhmeo  24915  bndth  24928  ismbf3d  25626  dvef  25955  reeff1o  26428  efifo  26527  dvloglem  26628  logf1o2  26630  bday1  27825  oniso  28282  dfn0s2  28343  bdayn0sf1o  28381  dfnns2  28383  choc1  31419  shsidmi  31476  shsval2i  31479  omlsii  31495  chdmm1i  31569  chj1i  31581  chm0i  31582  shjshsi  31584  span0  31634  spanuni  31636  sshhococi  31638  spansni  31649  pjoml4i  31679  pjrni  31794  shatomistici  32453  sumdmdlem2  32511  rinvf1o  32724  sigapildsys  34344  sxbrsigalem0  34453  dya2iocucvr  34466  sxbrsigalem4  34469  sxbrsiga  34472  ballotth  34720  kur14lem6  35431  mrsubrn  35733  msubrn  35749  filnetlem3  36600  filnetlem4  36601  onint1  36669  oninhaus  36670  bj-rabtr  37182  bj-rabtrAUTO  37184  bj-disj2r  37280  bj-nuliotaALT  37310  bj-idres  37419  icoreunrn  37618  dmsucmap  38723  comptiunov2i  44066  unisnALT  45285  fsumiunss  45939  fourierdlem62  46530  fouriersw  46593  salexct  46696  salgencntex  46705