Description: Restricted universal quantification on a subset in terms of superset. (Contributed by Stefan O'Rear, 3-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | ralss | ⊢ ( 𝐴 ⊆ 𝐵 → ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ 𝐴 → 𝜑 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssel | ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ) | |
2 | 1 | pm4.71rd | ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) ) ) |
3 | 2 | imbi1d | ⊢ ( 𝐴 ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝜑 ) ) ) |
4 | impexp | ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝜑 ) ↔ ( 𝑥 ∈ 𝐵 → ( 𝑥 ∈ 𝐴 → 𝜑 ) ) ) | |
5 | 3 4 | bitrdi | ⊢ ( 𝐴 ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ( 𝑥 ∈ 𝐵 → ( 𝑥 ∈ 𝐴 → 𝜑 ) ) ) ) |
6 | 5 | ralbidv2 | ⊢ ( 𝐴 ⊆ 𝐵 → ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ 𝐴 → 𝜑 ) ) ) |