Theorem ssralv2

Description: Quantification restricted to a subclass for two quantifiers. ssralv for two quantifiers. The proof of ssralv2 was automatically generated by minimizing the automatically translated proof of ssralv2VD . The automatic translation is by the tools program translate__without__overwriting.cmd. (Contributed by Alan Sare, 18-Feb-2012) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	ssralv2	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐷 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		nfv	⊢ Ⅎ 𝑥 ( 𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷 )
2		nfra1	⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐷 𝜑
3		ssralv	⊢ ( 𝐴 ⊆ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐷 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐷 𝜑 ) )
4	3	adantr	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐷 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐷 𝜑 ) )
5		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐷 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐷 𝜑 ) )
6	4 5	imbitrdi	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐷 𝜑 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐷 𝜑 ) ) )
7		sp	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐷 𝜑 ) → ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐷 𝜑 ) )
8	6 7	syl6	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐷 𝜑 → ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐷 𝜑 ) ) )
9		ssralv	⊢ ( 𝐶 ⊆ 𝐷 → ( ∀ 𝑦 ∈ 𝐷 𝜑 → ∀ 𝑦 ∈ 𝐶 𝜑 ) )
10	9	adantl	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷 ) → ( ∀ 𝑦 ∈ 𝐷 𝜑 → ∀ 𝑦 ∈ 𝐶 𝜑 ) )
11	8 10	syl6d	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐷 𝜑 → ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐶 𝜑 ) ) )
12	1 2 11	ralrimd	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐷 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐶 𝜑 ) )