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

Metamath Proof Explorer

Theorem r19.12

Description: Restricted quantifier version of 19.12 . (Contributed by NM, 15-Oct-2003) (Proof shortened by Andrew Salmon, 30-May-2011) Avoid ax-13 , ax-ext . (Revised by Wolf Lammen, 17-Jun-2023) (Proof shortened by Wolf Lammen, 4-Nov-2024)

Ref Expression
Assertion r19.12 ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 → ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 )

Proof

Step Hyp Ref Expression
1 df-rex ⊢ ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 𝜑 ) )
2 nfv ⊢ Ⅎ 𝑦 𝑥 ∈ 𝐴
3 nfra1 ⊢ Ⅎ 𝑦 ∀ 𝑦 ∈ 𝐵 𝜑
4 2 3 nfan ⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 𝜑 )
5 4 nfex ⊢ Ⅎ 𝑦 ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 𝜑 )
6 1 5 nfxfr ⊢ Ⅎ 𝑦 ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑
7 rsp ⊢ ( ∀ 𝑦 ∈ 𝐵 𝜑 → ( 𝑦 ∈ 𝐵 → 𝜑 ) )
8 7 com12 ⊢ ( 𝑦 ∈ 𝐵 → ( ∀ 𝑦 ∈ 𝐵 𝜑 → 𝜑 ) )
9 8 reximdv ⊢ ( 𝑦 ∈ 𝐵 → ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜑 ) )
10 9 com12 ⊢ ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 → ( 𝑦 ∈ 𝐵 → ∃ 𝑥 ∈ 𝐴 𝜑 ) )
11 6 10 ralrimi ⊢ ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 → ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 )