Theorem eqssi 3604

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

Syntax hints:   = wceq 1480   ⊆ wss 3560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-in 3567  df-ss 3574

This theorem is referenced by:  inv1  3948  unv  3949  intab  4479  intabs  4795  intid  4897  dmv  5311  0ima  5451  fresaunres2  6043  find  7053  dftpos4  7331  wfrlem16  7390  dfom3  8504  tc2  8578  tcidm  8582  tc0  8583  rankuni  8686  rankval4  8690  ackbij1  9020  cfom  9046  fin23lem16  9117  itunitc  9203  inaprc  9618  nqerf  9712  dmrecnq  9750  dmaddsr  9866  dmmulsr  9867  axaddf  9926  axmulf  9927  dfnn2  10993  dfuzi  11428  unirnioo  12231  uzrdgfni  12713  0bits  15104  4sqlem19  15610  ledm  17164  lern  17165  efgsfo  18092  0frgp  18132  indiscld  20835  leordtval2  20956  lecldbas  20963  llyidm  21231  nllyidm  21232  toplly  21233  lly1stc  21239  txuni2  21308  txindis  21377  ust0  21963  qdensere  22513  xrtgioo  22549  zdis  22559  xrhmeo  22685  bndth  22697  ismbf3d  23361  dvef  23681  reeff1o  24139  efifo  24231  dvloglem  24328  logf1o2  24330  choc1  28074  shsidmi  28131  shsval2i  28134  omlsii  28150  chdmm1i  28224  chj1i  28236  chm0i  28237  shjshsi  28239  span0  28289  spanuni  28291  sshhococi  28293  spansni  28304  pjoml4i  28334  pjrni  28449  shatomistici  29108  sumdmdlem2  29166  rinvf1o  29317  sigapildsys  30048  sxbrsigalem0  30156  dya2iocucvr  30169  sxbrsigalem4  30172  sxbrsiga  30175  ballotth  30422  kur14lem6  30954  mrsubrn  31171  msubrn  31187  filnetlem3  32070  filnetlem4  32071  onint1  32143  oninhaus  32144  bj-rabtr  32626  bj-rabtrALTALT  32628  bj-rabtrAUTO  32629  bj-disj2r  32713  bj-nuliotaALT  32720  icoreunrn  32878  comptiunov2i  37518  compneOLD  38165  unisnALT  38684  fsumiunss  39243  fourierdlem62  39722  fouriersw  39785  salexct  39889  salgencntex  39898