Theorem eqssi 2074

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

Hypotheses

Ref	Expression
eqssi.1	|- A (_ B
eqssi.2	|- B (_ A

Assertion

Ref	Expression
eqssi	|- A = B

Proof of Theorem eqssi

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

Syntax hints:   = wceq 954   (_ wss 2043

This theorem is referenced by:  inv1 2295  unv 2296  intab 2555  intabs 2728  unipw 2751  find 3150  dmv 3322  0ima 3413  ecopoprdm 4299  abfii4 4544  dfom3 4610  rankval3 4661  rankuni2 4670  rankun 4671  rankuni 4678  rankval4 4682  cfom 4896  dmaddpq 5039  dmmulpq 5041  dmaddsr 5174  dmmulsr 5175  axaddopr 5245  axmulopr 5246  unirnioo 6343  reeff1o 7376  subbas2 7595  qdensere 7701  chcmh 9052  omlsi 9183  choc1 9229  shsidm 9295  shsumval2 9298  chm1 9317  chdmm1 9338  chj1 9350  chm0 9351  shjshs 9353  span0 9403  spanun 9405  sshhococ 9407  spansn 9419  pjoml4 9470  shatomistic 10225  sumdmdlem2 10282

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-in 2047  df-ss 2049

Copyright terms: Public domain