This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eqssd

Description: Equality deduction from two subclass relationships. Compare Theorem 4 of Suppes p. 22. (Contributed by NM, 27-Jun-2004)

Ref Expression
Hypotheses eqssd.1 ⊢ φ → A ⊆ B
eqssd.2 ⊢ φ → B ⊆ A
Assertion eqssd ⊢ φ → A = B

Proof

Step Hyp Ref Expression
1 eqssd.1 ⊢ φ → A ⊆ B
2 eqssd.2 ⊢ φ → B ⊆ A
3 eqss ⊢ A = B ↔ A ⊆ B ∧ B ⊆ A
4 1 2 3 sylanbrc ⊢ φ → A = B