This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐴 𝜓 ) )