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

Metamath Proof Explorer

Theorem r19.35

Description: Restricted quantifier version of 19.35 . (Contributed by NM, 20-Sep-2003) (Proof shortened by Wolf Lammen, 22-Dec-2024)

Ref Expression
Assertion r19.35 ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜓 ) )

Proof

Step Hyp Ref Expression
1 pm5.5 ⊢ ( 𝜑 → ( ( 𝜑 → 𝜓 ) ↔ 𝜓 ) )
2 1 ralrexbid ⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 → ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ↔ ∃ 𝑥 ∈ 𝐴 𝜓 ) )
3 2 biimpcd ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) → ( ∀ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜓 ) )
4 rexnal ⊢ ( ∃ 𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∀ 𝑥 ∈ 𝐴 𝜑 )
5 pm2.21 ⊢ ( ¬ 𝜑 → ( 𝜑 → 𝜓 ) )
6 5 reximi ⊢ ( ∃ 𝑥 ∈ 𝐴 ¬ 𝜑 → ∃ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) )
7 4 6 sylbir ⊢ ( ¬ ∀ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) )
8 ax-1 ⊢ ( 𝜓 → ( 𝜑 → 𝜓 ) )
9 8 reximi ⊢ ( ∃ 𝑥 ∈ 𝐴 𝜓 → ∃ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) )
10 7 9 ja ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜓 ) → ∃ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) )
11 3 10 impbii ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜓 ) )