Theorem ssralv2VD 45557

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

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 1940	. . . . 5 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → ∀𝑥(𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷))
2		hbra1 3302	. . . . 5 ⊢ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑥∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑)
3		idn1 45266	. . . . . . . 8 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ▶   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   )
4		simpr 489	. . . . . . . 8 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → 𝐶 ⊆ 𝐷)
5	3, 4	e1a 45319	. . . . . . 7 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ▶   𝐶 ⊆ 𝐷   )
6		idn3 45307	. . . . . . . 8 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ,   𝑥 ∈ 𝐴   ▶   𝑥 ∈ 𝐴   )
7		simpl 487	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → 𝐴 ⊆ 𝐵)
8	3, 7	e1a 45319	. . . . . . . . . . 11 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ▶   𝐴 ⊆ 𝐵   )
9		idn2 45305	. . . . . . . . . . 11 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ▶   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   )
10		ssralv 4007	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐷 𝜑))
11	8, 9, 10	e12 45415	. . . . . . . . . 10 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ▶   ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐷 𝜑   )
12		df-ral 3080	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐷 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷 𝜑))
13	12	biimpi 219	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷 𝜑))
14	11, 13	e2 45323	. . . . . . . . 9 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ▶   ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷 𝜑)   )
15		sp 2219	. . . . . . . . 9 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷 𝜑) → (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷 𝜑))
16	14, 15	e2 45323	. . . . . . . 8 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ▶   (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷 𝜑)   )
17		pm2.27 43	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐴 → ((𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷 𝜑) → ∀𝑦 ∈ 𝐷 𝜑))
18	6, 16, 17	e32 45449	. . . . . . 7 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ,   𝑥 ∈ 𝐴   ▶   ∀𝑦 ∈ 𝐷 𝜑   )
19		ssralv 4007	. . . . . . 7 ⊢ (𝐶 ⊆ 𝐷 → (∀𝑦 ∈ 𝐷 𝜑 → ∀𝑦 ∈ 𝐶 𝜑))
20	5, 18, 19	e13 45439	. . . . . 6 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ,   𝑥 ∈ 𝐴   ▶   ∀𝑦 ∈ 𝐶 𝜑   )
21	20	in3 45301	. . . . 5 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ▶   (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐶 𝜑)   )
22	1, 2, 21	gen21nv 45312	. . . 4 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ▶   ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐶 𝜑)   )
23		df-ral 3080	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐶 𝜑))
24	23	biimpri 231	. . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐶 𝜑) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝜑)
25	22, 24	e2 45323	. . 3 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ▶   ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝜑   )
26	25	in2 45297	. 2 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ▶   (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝜑)   )
27	26	in1 45263	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝜑))

Syntax hints:   → wi 4   ∧ wa 400  ∀wal 1568   ∈ wcel 2143  ∀wral 3079   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-10 2176  ax-12 2213

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-ex 1810  df-nf 1814  df-ral 3080  df-ss 3923  df-vd1 45262  df-vd2 45270  df-vd3 45282

This theorem is referenced by: (None)