Metamath Proof Explorer


Theorem ssralv

Description: Quantification restricted to a subclass. (Contributed by NM, 11-Mar-2006) Avoid axioms. (Revised by GG, 19-May-2025)

Ref Expression
Assertion ssralv ( 𝐴𝐵 → ( ∀ 𝑥𝐵 𝜑 → ∀ 𝑥𝐴 𝜑 ) )

Proof

Step Hyp Ref Expression
1 df-ss ( 𝐴𝐵 ↔ ∀ 𝑥 ( 𝑥𝐴𝑥𝐵 ) )
2 imim1 ( ( 𝑥𝐴𝑥𝐵 ) → ( ( 𝑥𝐵𝜑 ) → ( 𝑥𝐴𝜑 ) ) )
3 2 al2imi ( ∀ 𝑥 ( 𝑥𝐴𝑥𝐵 ) → ( ∀ 𝑥 ( 𝑥𝐵𝜑 ) → ∀ 𝑥 ( 𝑥𝐴𝜑 ) ) )
4 df-ral ( ∀ 𝑥𝐵 𝜑 ↔ ∀ 𝑥 ( 𝑥𝐵𝜑 ) )
5 df-ral ( ∀ 𝑥𝐴 𝜑 ↔ ∀ 𝑥 ( 𝑥𝐴𝜑 ) )
6 3 4 5 3imtr4g ( ∀ 𝑥 ( 𝑥𝐴𝑥𝐵 ) → ( ∀ 𝑥𝐵 𝜑 → ∀ 𝑥𝐴 𝜑 ) )
7 1 6 sylbi ( 𝐴𝐵 → ( ∀ 𝑥𝐵 𝜑 → ∀ 𝑥𝐴 𝜑 ) )