Theorem eqssi 3760

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

Syntax hints:   = wceq 1632   ⊆ wss 3715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-in 3722  df-ss 3729

This theorem is referenced by:  inv1  4113  unv  4114  intab  4659  intabs  4974  intid  5075  dmv  5496  0ima  5640  fresaunres2  6237  find  7256  dftpos4  7540  wfrlem16  7599  dfom3  8717  tc2  8791  tcidm  8795  tc0  8796  rankuni  8899  rankval4  8903  djuun  8950  ackbij1  9252  cfom  9278  fin23lem16  9349  itunitc  9435  inaprc  9850  nqerf  9944  dmrecnq  9982  dmaddsr  10098  dmmulsr  10099  axaddf  10158  axmulf  10159  dfnn2  11225  dfuzi  11660  unirnioo  12466  uzrdgfni  12951  0bits  15363  4sqlem19  15869  ledm  17425  lern  17426  efgsfo  18352  0frgp  18392  indiscld  21097  leordtval2  21218  lecldbas  21225  llyidm  21493  nllyidm  21494  toplly  21495  lly1stc  21501  txuni2  21570  txindis  21639  ust0  22224  qdensere  22774  xrtgioo  22810  zdis  22820  xrhmeo  22946  bndth  22958  ismbf3d  23620  dvef  23942  reeff1o  24400  efifo  24492  dvloglem  24593  logf1o2  24595  choc1  28495  shsidmi  28552  shsval2i  28555  omlsii  28571  chdmm1i  28645  chj1i  28657  chm0i  28658  shjshsi  28660  span0  28710  spanuni  28712  sshhococi  28714  spansni  28725  pjoml4i  28755  pjrni  28870  shatomistici  29529  sumdmdlem2  29587  rinvf1o  29741  sigapildsys  30534  sxbrsigalem0  30642  dya2iocucvr  30655  sxbrsigalem4  30658  sxbrsiga  30661  ballotth  30908  kur14lem6  31500  mrsubrn  31717  msubrn  31733  filnetlem3  32681  filnetlem4  32682  onint1  32754  oninhaus  32755  bj-rabtr  33232  bj-rabtrALTALT  33234  bj-rabtrAUTO  33235  bj-disj2r  33319  bj-nuliotaALT  33326  icoreunrn  33518  idinxpres  34412  comptiunov2i  38500  compneOLD  39146  unisnALT  39661  fsumiunss  40310  fourierdlem62  40888  fouriersw  40951  salexct  41055  salgencntex  41064