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

Metamath Proof Explorer

Theorem ralss

Description: Restricted universal quantification on a subset in terms of superset. (Contributed by Stefan O'Rear, 3-Apr-2015) Avoid axioms. (Revised by SN, 14-Oct-2025)

Ref Expression
Assertion ralss ⊢ A ⊆ B → ∀ x ∈ A φ ↔ ∀ x ∈ B x ∈ A → φ

Proof

Step Hyp Ref Expression
1 df-ss ⊢ A ⊆ B ↔ ∀ x x ∈ A → x ∈ B
2 id ⊢ x ∈ A → x ∈ B → x ∈ A → x ∈ B
3 2 pm4.71rd ⊢ x ∈ A → x ∈ B → x ∈ A ↔ x ∈ B ∧ x ∈ A
4 3 imbi1d ⊢ x ∈ A → x ∈ B → x ∈ A → φ ↔ x ∈ B ∧ x ∈ A → φ
5 impexp ⊢ x ∈ B ∧ x ∈ A → φ ↔ x ∈ B → x ∈ A → φ
6 4 5 bitrdi ⊢ x ∈ A → x ∈ B → x ∈ A → φ ↔ x ∈ B → x ∈ A → φ
7 6 alimi ⊢ ∀ x x ∈ A → x ∈ B → ∀ x x ∈ A → φ ↔ x ∈ B → x ∈ A → φ
8 1 7 sylbi ⊢ A ⊆ B → ∀ x x ∈ A → φ ↔ x ∈ B → x ∈ A → φ
9 albi ⊢ ∀ x x ∈ A → φ ↔ x ∈ B → x ∈ A → φ → ∀ x x ∈ A → φ ↔ ∀ x x ∈ B → x ∈ A → φ
10 8 9 syl ⊢ A ⊆ B → ∀ x x ∈ A → φ ↔ ∀ x x ∈ B → x ∈ A → φ
11 df-ral ⊢ ∀ x ∈ A φ ↔ ∀ x x ∈ A → φ
12 df-ral ⊢ ∀ x ∈ B x ∈ A → φ ↔ ∀ x x ∈ B → x ∈ A → φ
13 10 11 12 3bitr4g ⊢ A ⊆ B → ∀ x ∈ A φ ↔ ∀ x ∈ B x ∈ A → φ