Theorem eqssi 3938

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

Syntax hints:   = wceq 1542   ⊆ wss 3889

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 2708

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

This theorem is referenced by:  inv1  4338  unv  4339  intab  4920  intabs  5290  dmv  5877  0ima  6043  cnvrescnv  6159  find  7846  dftpos4  8195  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  12187  dfuzi  12620  unirnioo  13402  uzrdgfni  13920  0bits  16408  4sqlem19  16934  ledm  18556  lern  18557  efgsfo  19714  0frgp  19754  indiscld  23056  leordtval2  23177  lecldbas  23184  llyidm  23453  nllyidm  23454  toplly  23455  lly1stc  23461  txuni2  23530  txindis  23599  ust0  24185  qdensere  24734  xrtgioo  24772  zdis  24782  xrhmeo  24913  bndth  24925  ismbf3d  25621  dvef  25947  reeff1o  26412  efifo  26511  dvloglem  26612  logf1o2  26614  bday1  27806  oniso  28263  dfn0s2  28324  bdayn0sf1o  28362  dfnns2  28364  choc1  31398  shsidmi  31455  shsval2i  31458  omlsii  31474  chdmm1i  31548  chj1i  31560  chm0i  31561  shjshsi  31563  span0  31613  spanuni  31615  sshhococi  31617  spansni  31628  pjoml4i  31658  pjrni  31773  shatomistici  32432  sumdmdlem2  32490  rinvf1o  32703  sigapildsys  34306  sxbrsigalem0  34415  dya2iocucvr  34428  sxbrsigalem4  34431  sxbrsiga  34434  ballotth  34682  kur14lem6  35393  mrsubrn  35695  msubrn  35711  filnetlem3  36562  filnetlem4  36563  onint1  36631  oninhaus  36632  ttcuniun  36692  ttciunun  36693  ttcuni  36695  dfttc4  36712  bj-rabtr  37237  bj-rabtrAUTO  37239  bj-disj2r  37335  bj-nuliotaALT  37365  bj-idres  37474  icoreunrn  37675  dmsucmap  38789  comptiunov2i  44133  unisnALT  45352  fsumiunss  46005  fourierdlem62  46596  fouriersw  46659  salexct  46762  salgencntex  46771