Theorem eqssi 3983

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

Syntax hints:   = wceq 1537   ⊆ wss 3936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952

This theorem is referenced by:  inv1  4348  unv  4349  intab  4906  intabs  5245  intid  5350  dmv  5792  0ima  5946  cnvrescnv  6052  find  7607  dftpos4  7911  wfrlem16  7970  dfom3  9110  tc2  9184  tcidm  9188  tc0  9189  rankuni  9292  rankval4  9296  djuunxp  9350  djuun  9355  ackbij1  9660  cfom  9686  fin23lem16  9757  itunitc  9843  inaprc  10258  nqerf  10352  dmrecnq  10390  dmaddsr  10507  dmmulsr  10508  axaddf  10567  axmulf  10568  dfnn2  11651  dfuzi  12074  unirnioo  12838  uzrdgfni  13327  0bits  15788  4sqlem19  16299  ledm  17834  lern  17835  efgsfo  18865  0frgp  18905  indiscld  21699  leordtval2  21820  lecldbas  21827  llyidm  22096  nllyidm  22097  toplly  22098  lly1stc  22104  txuni2  22173  txindis  22242  ust0  22828  qdensere  23378  xrtgioo  23414  zdis  23424  xrhmeo  23550  bndth  23562  ismbf3d  24255  dvef  24577  reeff1o  25035  efifo  25131  dvloglem  25231  logf1o2  25233  choc1  29104  shsidmi  29161  shsval2i  29164  omlsii  29180  chdmm1i  29254  chj1i  29266  chm0i  29267  shjshsi  29269  span0  29319  spanuni  29321  sshhococi  29323  spansni  29334  pjoml4i  29364  pjrni  29479  shatomistici  30138  sumdmdlem2  30196  rinvf1o  30375  sigapildsys  31421  sxbrsigalem0  31529  dya2iocucvr  31542  sxbrsigalem4  31545  sxbrsiga  31548  ballotth  31795  kur14lem6  32458  mrsubrn  32760  msubrn  32776  filnetlem3  33728  filnetlem4  33729  onint1  33797  oninhaus  33798  bj-rabtr  34251  bj-rabtrAUTO  34253  bj-disj2r  34343  bj-nuliotaALT  34354  bj-idres  34455  icoreunrn  34643  comptiunov2i  40071  unisnALT  41280  fsumiunss  41876  fourierdlem62  42473  fouriersw  42536  salexct  42637  salgencntex  42646