Theorem ssralv2VD 45218

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

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 1912	. . . . 5 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → ∀𝑥(𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷))
2		hbra1 3275	. . . . 5 ⊢ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑥∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑)
3		idn1 44927	. . . . . . . 8 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ▶   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   )
4		simpr 484	. . . . . . . 8 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → 𝐶 ⊆ 𝐷)
5	3, 4	e1a 44980	. . . . . . 7 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ▶   𝐶 ⊆ 𝐷   )
6		idn3 44968	. . . . . . . 8 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ,   𝑥 ∈ 𝐴   ▶   𝑥 ∈ 𝐴   )
7		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → 𝐴 ⊆ 𝐵)
8	3, 7	e1a 44980	. . . . . . . . . . 11 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ▶   𝐴 ⊆ 𝐵   )
9		idn2 44966	. . . . . . . . . . 11 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ▶   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   )
10		ssralv 4004	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐷 𝜑))
11	8, 9, 10	e12 45076	. . . . . . . . . 10 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ▶   ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐷 𝜑   )
12		df-ral 3053	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐷 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷 𝜑))
13	12	biimpi 216	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷 𝜑))
14	11, 13	e2 44984	. . . . . . . . 9 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ▶   ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷 𝜑)   )
15		sp 2191	. . . . . . . . 9 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷 𝜑) → (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷 𝜑))
16	14, 15	e2 44984	. . . . . . . 8 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ▶   (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷 𝜑)   )
17		pm2.27 42	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐴 → ((𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐷 𝜑) → ∀𝑦 ∈ 𝐷 𝜑))
18	6, 16, 17	e32 45110	. . . . . . 7 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ,   𝑥 ∈ 𝐴   ▶   ∀𝑦 ∈ 𝐷 𝜑   )
19		ssralv 4004	. . . . . . 7 ⊢ (𝐶 ⊆ 𝐷 → (∀𝑦 ∈ 𝐷 𝜑 → ∀𝑦 ∈ 𝐶 𝜑))
20	5, 18, 19	e13 45100	. . . . . 6 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ,   𝑥 ∈ 𝐴   ▶   ∀𝑦 ∈ 𝐶 𝜑   )
21	20	in3 44962	. . . . 5 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ▶   (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐶 𝜑)   )
22	1, 2, 21	gen21nv 44973	. . . 4 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ▶   ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐶 𝜑)   )
23		df-ral 3053	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐶 𝜑))
24	23	biimpri 228	. . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐶 𝜑) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝜑)
25	22, 24	e2 44984	. . 3 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ,   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑   ▶   ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝜑   )
26	25	in2 44958	. 2 ⊢ (   (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)   ▶   (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝜑)   )
27	26	in1 44924	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝜑))

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1540   ∈ wcel 2114  ∀wral 3052   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-10 2147  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-ex 1782  df-nf 1786  df-ral 3053  df-ss 3920  df-vd1 44923  df-vd2 44931  df-vd3 44943

This theorem is referenced by: (None)