Theorem ssralv2 44563

Description: Quantification restricted to a subclass for two quantifiers. ssralv 4003 for two quantifiers. The proof of ssralv2 44563 was automatically generated by minimizing the automatically translated proof of ssralv2VD 44897. 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.)

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐶   𝑦,𝐶   𝑥,𝐷   𝑦,𝐷

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑦)   𝐵(𝑦)

Proof of Theorem ssralv2

Step	Hyp	Ref	Expression
1		nfv 1915	. 2 ⊢ Ⅎ𝑥(𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)
2		nfra1 3256	. 2 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑
3		ssralv 4003	. . . . . 6 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐷 𝜑))
4	3	adantr 480	. . . . 5 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐷 𝜑))
5		df-ral 3048	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐷 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷 𝜑))
6	4, 5	imbitrdi 251	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷 𝜑)))
7		sp 2186	. . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷 𝜑) → (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷 𝜑))
8	6, 7	syl6 35	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑 → (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷 𝜑)))
9		ssralv 4003	. . . 4 ⊢ (𝐶 ⊆ 𝐷 → (∀𝑦 ∈ 𝐷 𝜑 → ∀𝑦 ∈ 𝐶 𝜑))
10	9	adantl 481	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (∀𝑦 ∈ 𝐷 𝜑 → ∀𝑦 ∈ 𝐶 𝜑))
11	8, 10	syl6d 75	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑 → (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐶 𝜑)))
12	1, 2, 11	ralrimd 3237	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝜑))

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1539   ∈ wcel 2111  ∀wral 3047   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-10 2144  ax-12 2180

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-nf 1785  df-ral 3048  df-ss 3919

This theorem is referenced by:  ordelordALT  44569  ordelordALTVD  44898