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

Metamath Proof Explorer

Theorem relssi

Description: Inference from subclass principle for relations. (Contributed by NM, 31-Mar-1998)

Ref Expression
Hypotheses relssi.1 ⊢ Rel ⁡ A
relssi.2 ⊢ x y ∈ A → x y ∈ B
Assertion relssi ⊢ A ⊆ B

Proof

Step Hyp Ref Expression
1 relssi.1 ⊢ Rel ⁡ A
2 relssi.2 ⊢ x y ∈ A → x y ∈ B
3 ssrel ⊢ Rel ⁡ A → A ⊆ B ↔ ∀ x ∀ y x y ∈ A → x y ∈ B
4 1 3 ax-mp ⊢ A ⊆ B ↔ ∀ x ∀ y x y ∈ A → x y ∈ B
5 2 ax-gen ⊢ ∀ y x y ∈ A → x y ∈ B
6 4 5 mpgbir ⊢ A ⊆ B