Theorem eqssi 3929

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

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  inv1  4351  unv  4352  intab  4943  intabs  5317  dmv  5916  cnvrescnv  6206  0ima  6219  find  7941  dftpos4  8300  dfom3  9685  dmttrcl  9759  rnttrcl  9760  tc2  9778  tcidm  9782  tc0  9783  rankuni  9916  rankval4  9921  djuunxp  10039  djuun  10044  ackbij1  10354  cfom  10381  fin23lem16  10452  itunitc  10538  inaprc  10960  nqerf  11054  dmrecnq  11092  dmaddsr  11209  dmmulsr  11210  axaddf  11269  axmulf  11270  dfnn2  12388  dfuzi  12830  unirnioo  13620  uzrdgfni  14141  sgnrn  15294  0bits  16653  4sqlem19  17185  ledm  18814  lern  18815  efgsfo  20004  0frgp  20044  indiscld  23464  leordtval2  23585  lecldbas  23592  llyidm  23862  nllyidm  23863  toplly  23864  lly1stc  23870  txuni2  23939  txindis  24008  ust0  24594  qdensere  25143  xrtgioo  25181  zdis  25191  xrhmeo  25322  bndth  25334  ismbf3d  26030  dvef  26355  reeff1o  26831  efifo  26932  dvloglem  27033  logf1o2  27035  bday1  28257  oniso  28714  dfn0s2  28775  bdayn0sf1o  28813  dfnns2  28815  choc1  31986  shsidmi  32043  shsval2i  32046  omlsii  32062  chdmm1i  32136  chj1i  32148  chm0i  32149  shjshsi  32151  span0  32201  spanuni  32203  sshhococi  32205  spansni  32216  pjoml4i  32246  pjrni  32361  shatomistici  33020  sumdmdlem2  33078  rinvf1o  33322  sigapildsys  34906  sxbrsigalem0  35014  dya2iocucvr  35027  sxbrsigalem4  35030  sxbrsiga  35033  ballotth  35281  scottidm  35882  jf1o  36052  kur14lem6  36184  mrsubrn  36486  msubrn  36502  filnetlem3  37383  filnetlem4  37384  onint1  37452  oninhaus  37453  ttcuniun  37513  ttciunun  37514  ttcuni  37516  dfttc4  37533  bj-rabtr  38058  bj-rabtrAUTO  38060  bj-disj2r  38156  bj-nuliotaALT  38243  bj-idres  38349  icoreunrn  38550  dfprop  38915  dmsucmap  39666  comptiunov2i  44967  unisnALT  46168  fsumiunss  46860  fourierdlem62  47451  fouriersw  47514  salexct  47617  salgencntex  47626