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 711	1 ⊢ 𝐴 = 𝐵

Syntax hints:   = wceq 1540   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  inv1  4349  unv  4350  intab  4928  intabs  5288  intidOLD  5401  dmv  5865  0ima  6029  cnvrescnv  6144  find  7828  dftpos4  8178  dfom3  9543  dmttrcl  9617  rnttrcl  9618  tc2  9638  tcidm  9642  tc0  9643  rankuni  9759  rankval4  9763  djuunxp  9817  djuun  9822  ackbij1  10131  cfom  10158  fin23lem16  10229  itunitc  10315  inaprc  10730  nqerf  10824  dmrecnq  10862  dmaddsr  10979  dmmulsr  10980  axaddf  11039  axmulf  11040  dfnn2  12141  dfuzi  12567  unirnioo  13352  uzrdgfni  13865  0bits  16350  4sqlem19  16875  ledm  18496  lern  18497  efgsfo  19618  0frgp  19658  indiscld  22976  leordtval2  23097  lecldbas  23104  llyidm  23373  nllyidm  23374  toplly  23375  lly1stc  23381  txuni2  23450  txindis  23519  ust0  24105  qdensere  24655  xrtgioo  24693  zdis  24703  xrhmeo  24842  bndth  24855  ismbf3d  25553  dvef  25882  reeff1o  26355  efifo  26454  dvloglem  26555  logf1o2  26557  bday1s  27745  onsiso  28174  dfn0s2  28229  bdayn0sf1o  28264  dfnns2  28266  choc1  31271  shsidmi  31328  shsval2i  31331  omlsii  31347  chdmm1i  31421  chj1i  31433  chm0i  31434  shjshsi  31436  span0  31486  spanuni  31488  sshhococi  31490  spansni  31501  pjoml4i  31531  pjrni  31646  shatomistici  32305  sumdmdlem2  32363  rinvf1o  32574  sigapildsys  34135  sxbrsigalem0  34245  dya2iocucvr  34258  sxbrsigalem4  34261  sxbrsiga  34264  ballotth  34512  kur14lem6  35194  mrsubrn  35496  msubrn  35512  filnetlem3  36364  filnetlem4  36365  onint1  36433  oninhaus  36434  bj-rabtr  36914  bj-rabtrAUTO  36916  bj-disj2r  37012  bj-nuliotaALT  37042  bj-idres  37144  icoreunrn  37343  comptiunov2i  43689  unisnALT  44909  fsumiunss  45566  fourierdlem62  46159  fouriersw  46222  salexct  46325  salgencntex  46334