Theorem ssralv2 44502

Description: Quantification restricted to a subclass for two quantifiers. ssralv 4077 for two quantifiers. The proof of ssralv2 44502 was automatically generated by minimizing the automatically translated proof of ssralv2VD 44837. 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 1913	. 2 ⊢ Ⅎ𝑥(𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)
2		nfra1 3290	. 2 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑
3		ssralv 4077	. . . . . 6 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐷 𝜑))
4	3	adantr 480	. . . . 5 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐷 𝜑))
5		df-ral 3068	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐷 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷 𝜑))
6	4, 5	imbitrdi 251	. . . 4 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷 𝜑)))
7		sp 2184	. . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷 𝜑) → (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷 𝜑))
8	6, 7	syl6 35	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑 → (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷 𝜑)))
9		ssralv 4077	. . . 4 ⊢ (𝐶 ⊆ 𝐷 → (∀𝑦 ∈ 𝐷 𝜑 → ∀𝑦 ∈ 𝐶 𝜑))
10	9	adantl 481	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (∀𝑦 ∈ 𝐷 𝜑 → ∀𝑦 ∈ 𝐶 𝜑))
11	8, 10	syl6d 75	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑 → (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐶 𝜑)))
12	1, 2, 11	ralrimd 3270	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝜑))

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1535   ∈ wcel 2108  ∀wral 3067   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-10 2141  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-ex 1778  df-nf 1782  df-ral 3068  df-ss 3993

This theorem is referenced by:  ordelordALT  44508  ordelordALTVD  44838