Theorem ssralv2VD 44904

Description: Quantification restricted to a subclass for two quantifiers. ssralv 4003 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 44570 is ssralv2VD 44904 without virtual deductions and was automatically derived from ssralv2VD 44904.

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 1911	. . . . 5 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → ∀𝑥(𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷))
2		hbra1 3269	. . . . 5 ⊢ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑥∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑)
3		idn1 44613	. . . . . . . 8 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ▶   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   )
4		simpr 484	. . . . . . . 8 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → 𝐶 ⊆ 𝐷)
5	3, 4	e1a 44666	. . . . . . 7 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ▶   𝐶 ⊆ 𝐷   )
6		idn3 44654	. . . . . . . 8 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ,   𝑥 ∈ 𝐴   ▶   𝑥 ∈ 𝐴   )
7		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → 𝐴 ⊆ 𝐵)
8	3, 7	e1a 44666	. . . . . . . . . . 11 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ▶   𝐴 ⊆ 𝐵   )
9		idn2 44652	. . . . . . . . . . 11 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ▶   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   )
10		ssralv 4003	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐷 𝜑))
11	8, 9, 10	e12 44762	. . . . . . . . . 10 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ▶   ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐷 𝜑   )
12		df-ral 3048	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐷 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷 𝜑))
13	12	biimpi 216	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷 𝜑))
14	11, 13	e2 44670	. . . . . . . . 9 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ▶   ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷 𝜑)   )
15		sp 2186	. . . . . . . . 9 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷 𝜑) → (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷 𝜑))
16	14, 15	e2 44670	. . . . . . . 8 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ▶   (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷 𝜑)   )
17		pm2.27 42	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐴 → ((𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷 𝜑) → ∀𝑦 ∈ 𝐷 𝜑))
18	6, 16, 17	e32 44796	. . . . . . 7 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ,   𝑥 ∈ 𝐴   ▶   ∀𝑦 ∈ 𝐷 𝜑   )
19		ssralv 4003	. . . . . . 7 ⊢ (𝐶 ⊆ 𝐷 → (∀𝑦 ∈ 𝐷 𝜑 → ∀𝑦 ∈ 𝐶 𝜑))
20	5, 18, 19	e13 44786	. . . . . 6 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ,   𝑥 ∈ 𝐴   ▶   ∀𝑦 ∈ 𝐶 𝜑   )
21	20	in3 44648	. . . . 5 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ▶   (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐶 𝜑)   )
22	1, 2, 21	gen21nv 44659	. . . 4 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ▶   ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐶 𝜑)   )
23		df-ral 3048	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐶 𝜑))
24	23	biimpri 228	. . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐶 𝜑) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝜑)
25	22, 24	e2 44670	. . 3 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ▶   ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝜑   )
26	25	in2 44644	. 2 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ▶   (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝜑)   )
27	26	in1 44610	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-3an 1088  df-ex 1781  df-nf 1785  df-ral 3048  df-ss 3919  df-vd1 44609  df-vd2 44617  df-vd3 44629

This theorem is referenced by: (None)