Theorem ssralv2VD 44886

Description: Quantification restricted to a subclass for two quantifiers. ssralv 4052 for two quantifiers. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. ssralv2 44551 is ssralv2VD 44886 without virtual deductions and was automatically derived from ssralv2VD 44886.

1::	⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ▶   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   )
2::	⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷𝜑   ▶   ∀𝑥 ∈ 𝐵∀𝑦 ∈ 𝐷𝜑   )
3:1:	⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ▶   𝐴 ⊆ 𝐵   )
4:3,2:	⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷𝜑   ▶   ∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐷𝜑   )
5:4:	⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷𝜑   ▶   ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷𝜑)   )
6:5:	⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷𝜑   ▶   (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷𝜑)   )
7::	⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷𝜑, 𝑥 ∈ 𝐴   ▶   𝑥 ∈ 𝐴   )
8:7,6:	⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷𝜑, 𝑥 ∈ 𝐴   ▶   ∀𝑦 ∈ 𝐷𝜑   )
9:1:	⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ▶   𝐶 ⊆ 𝐷   )
10:9,8:	⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷𝜑, 𝑥 ∈ 𝐴   ▶   ∀𝑦 ∈ 𝐶𝜑   )
11:10:	⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷𝜑   ▶   (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐶𝜑)   )
12::	⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → ∀𝑥(𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷))
13::	⊢ (∀𝑥 ∈ 𝐵∀𝑦 ∈ 𝐷𝜑 → ∀𝑥∀𝑥 ∈ 𝐵∀𝑦 ∈ 𝐷𝜑)
14:12,13,11:	⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷𝜑   ▶   ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐶𝜑)   )
15:14:	⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷𝜑   ▶   ∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐶𝜑   )
16:15:	⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)    ▶   (∀𝑥 ∈ 𝐵∀𝑦 ∈ 𝐷𝜑 → ∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐶𝜑)   )
qed:16:	⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (∀𝑥 ∈ 𝐵∀𝑦 ∈ 𝐷𝜑 → ∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐶𝜑))

(Contributed by Alan Sare, 10-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

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

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

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

Proof of Theorem ssralv2VD

Step	Hyp	Ref	Expression
1		ax-5 1910	. . . . 5 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → ∀𝑥(𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷))
2		hbra1 3301	. . . . 5 ⊢ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑥∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑)
3		idn1 44594	. . . . . . . 8 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ▶   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   )
4		simpr 484	. . . . . . . 8 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → 𝐶 ⊆ 𝐷)
5	3, 4	e1a 44647	. . . . . . 7 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ▶   𝐶 ⊆ 𝐷   )
6		idn3 44635	. . . . . . . 8 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ,   𝑥 ∈ 𝐴   ▶   𝑥 ∈ 𝐴   )
7		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → 𝐴 ⊆ 𝐵)
8	3, 7	e1a 44647	. . . . . . . . . . 11 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ▶   𝐴 ⊆ 𝐵   )
9		idn2 44633	. . . . . . . . . . 11 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ▶   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   )
10		ssralv 4052	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐷 𝜑))
11	8, 9, 10	e12 44744	. . . . . . . . . 10 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ▶   ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐷 𝜑   )
12		df-ral 3062	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐷 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷 𝜑))
13	12	biimpi 216	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷 𝜑))
14	11, 13	e2 44651	. . . . . . . . 9 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ▶   ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷 𝜑)   )
15		sp 2183	. . . . . . . . 9 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷 𝜑) → (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷 𝜑))
16	14, 15	e2 44651	. . . . . . . 8 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ▶   (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷 𝜑)   )
17		pm2.27 42	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐴 → ((𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷 𝜑) → ∀𝑦 ∈ 𝐷 𝜑))
18	6, 16, 17	e32 44778	. . . . . . 7 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ,   𝑥 ∈ 𝐴   ▶   ∀𝑦 ∈ 𝐷 𝜑   )
19		ssralv 4052	. . . . . . 7 ⊢ (𝐶 ⊆ 𝐷 → (∀𝑦 ∈ 𝐷 𝜑 → ∀𝑦 ∈ 𝐶 𝜑))
20	5, 18, 19	e13 44768	. . . . . 6 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ,   𝑥 ∈ 𝐴   ▶   ∀𝑦 ∈ 𝐶 𝜑   )
21	20	in3 44629	. . . . 5 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ▶   (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐶 𝜑)   )
22	1, 2, 21	gen21nv 44640	. . . 4 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ▶   ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐶 𝜑)   )
23		df-ral 3062	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐶 𝜑))
24	23	biimpri 228	. . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐶 𝜑) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝜑)
25	22, 24	e2 44651	. . 3 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ▶   ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝜑   )
26	25	in2 44625	. 2 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ▶   (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝜑)   )
27	26	in1 44591	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝜑))

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1538   ∈ wcel 2108  ∀wral 3061   ⊆ wss 3951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-10 2141  ax-12 2177

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-ex 1780  df-nf 1784  df-ral 3062  df-ss 3968  df-vd1 44590  df-vd2 44598  df-vd3 44610

This theorem is referenced by: (None)