Theorem rr19.28v

Description: Restricted quantifier version of Theorem 19.28 of Margaris p. 90. We don't need the nonempty class condition of r19.28zv when there is an outer quantifier. (Contributed by NM, 29-Oct-2012)

	Ref	Expression
Assertion	rr19.28v	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜑 )
2	1	ralimi	⊢ ( ∀ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) → ∀ 𝑦 ∈ 𝐴 𝜑 )
3		biidd	⊢ ( 𝑦 = 𝑥 → ( 𝜑 ↔ 𝜑 ) )
4	3	rspcv	⊢ ( 𝑥 ∈ 𝐴 → ( ∀ 𝑦 ∈ 𝐴 𝜑 → 𝜑 ) )
5	2 4	syl5	⊢ ( 𝑥 ∈ 𝐴 → ( ∀ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) → 𝜑 ) )
6		simpr	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜓 )
7	6	ralimi	⊢ ( ∀ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) → ∀ 𝑦 ∈ 𝐴 𝜓 )
8	5 7	jca2	⊢ ( 𝑥 ∈ 𝐴 → ( ∀ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) → ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 𝜓 ) ) )
9	8	ralimia	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) → ∀ 𝑥 ∈ 𝐴 ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 𝜓 ) )
10		r19.28v	⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 𝜓 ) → ∀ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) )
11	10	ralimi	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 𝜓 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) )
12	9 11	impbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 𝜓 ) )