Theorem eqssi 3947

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

This proof depends on syntax axioms:   = wceq 1570   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ss 3916

This theorem is used by:  inv1  4348  unv  4349  intab  4938  intabs  5310  dmv  5904  cnvrescnv  6188  0ima  6200  find  7907  dftpos4  8262  dfom3  9648  dmttrcl  9722  rnttrcl  9723  tc2  9741  tcidm  9745  tc0  9746  rankuni  9879  rankval4  9884  djuunxp  10002  djuun  10007  ackbij1  10315  cfom  10342  fin23lem16  10413  itunitc  10499  inaprc  10921  nqerf  11015  dmrecnq  11053  dmaddsr  11170  dmmulsr  11171  axaddf  11230  axmulf  11231  dfnn2  12348  dfuzi  12790  unirnioo  13580  uzrdgfni  14101  sgnrn  15251  0bits  16609  4sqlem19  17141  ledm  18764  lern  18765  efgsfo  19953  0frgp  19993  indiscld  23409  leordtval2  23530  lecldbas  23537  llyidm  23807  nllyidm  23808  toplly  23809  lly1stc  23815  txuni2  23884  txindis  23953  ust0  24539  qdensere  25088  xrtgioo  25126  zdis  25136  xrhmeo  25267  bndth  25279  ismbf3d  25975  dvef  26300  reeff1o  26774  efifo  26875  dvloglem  26976  logf1o2  26978  bday1  28200  oniso  28657  dfn0s2  28718  bdayn0sf1o  28756  dfnns2  28758  choc1  31929  shsidmi  31986  shsval2i  31989  omlsii  32005  chdmm1i  32079  chj1i  32091  chm0i  32092  shjshsi  32094  span0  32144  spanuni  32146  sshhococi  32148  spansni  32159  pjoml4i  32189  pjrni  32304  shatomistici  32963  sumdmdlem2  33021  rinvf1o  33224  sigapildsys  34795  sxbrsigalem0  34903  dya2iocucvr  34916  sxbrsigalem4  34919  sxbrsiga  34922  ballotth  35170  kur14lem6  35976  mrsubrn  36278  msubrn  36294  filnetlem3  37168  filnetlem4  37169  onint1  37237  oninhaus  37238  ttcuniun  37298  ttciunun  37299  ttcuni  37301  dfttc4  37318  bj-rabtr  37843  bj-rabtrAUTO  37845  bj-disj2r  37941  bj-nuliotaALT  37973  bj-idres  38081  icoreunrn  38282  dfprop  38647  dmsucmap  39400  comptiunov2i  44705  unisnALT  45907  fsumiunss  46586  fourierdlem62  47177  fouriersw  47240  salexct  47343  salgencntex  47352