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 ( 𝐴 ⊆ 𝐵 → ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ 𝐴 → 𝜑 ) ) )

Proof

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