Theorem eqssi 2632

Description: Infer equality from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22.

Hypotheses

Ref	Expression
eqssi.1	|- A C_ B
eqssi.2	|- B C_ A

Assertion

Ref	Expression
eqssi	|- A = B

Proof of Theorem eqssi

Step	Hyp	Ref	Expression
1		eqss 2631	. 2 |- (A = B <-> (A C_ B /\ B C_ A))
2		eqssi.1	. 2 |- A C_ B
3		eqssi.2	. 2 |- B C_ A
4	1, 2, 3	mpbir2an 800	1 |- A = B

Syntax hints:   = wceq 1298   C_ wss 2593

This theorem is referenced by:  inv1 2898  unv 2899  intab 3247  intabs 3469  intid 3512  find 3977  findOLD 3978  dmv 4174  0ima 4284  ecopoprdm 5368  abfii4 5654  dfom3 5737  rankval3 5792  rankuni2 5801  rankun 5802  rankuni 5809  rankval4 5813  cfom 6064  dmaddpq 6211  dmmulpq 6213  dmaddsr 6346  dmmulsr 6347  axaddopr 6417  axmulopr 6418  unirnioo 7571  reeff1o 8691  subbas2 8915  qdensere 9027  chcmhi 10746  omlsii 10878  choc1 10924  shsidmi 10990  shsumval2i 10993  chm1i 11012  chdmm1i 11033  chj1i 11045  chm0i 11046  shjshsi 11048  span0 11098  spanuni 11100  sshhococi 11102  spansni 11113  pjoml4i 11163  shatomistici 11933  sumdmdlem2 11991  wfrlem16 13972  residcp 14392  fneerdm 15498  txmet 15925  strbi 16712

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-10 1308  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-in 2603  df-ss 2605

Copyright terms: Public domain