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

Metamath Proof Explorer

Theorem r19.43

Description: Restricted quantifier version of 19.43 . (Contributed by NM, 27-May-1998) (Proof shortened by Andrew Salmon, 30-May-2011)

Ref Expression
Assertion r19.43 ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∨ 𝜓 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∨ ∃ 𝑥 ∈ 𝐴 𝜓 ) )

Proof

Step Hyp Ref Expression
1 r19.35 ⊢ ( ∃ 𝑥 ∈ 𝐴 ( ¬ 𝜑 → 𝜓 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜓 ) )
2 df-or ⊢ ( ( 𝜑 ∨ 𝜓 ) ↔ ( ¬ 𝜑 → 𝜓 ) )
3 2 rexbii ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∨ 𝜓 ) ↔ ∃ 𝑥 ∈ 𝐴 ( ¬ 𝜑 → 𝜓 ) )
4 df-or ⊢ ( ( ∃ 𝑥 ∈ 𝐴 𝜑 ∨ ∃ 𝑥 ∈ 𝐴 𝜓 ) ↔ ( ¬ ∃ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜓 ) )
5 ralnex ⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃ 𝑥 ∈ 𝐴 𝜑 )
6 5 imbi1i ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜓 ) ↔ ( ¬ ∃ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜓 ) )
7 4 6 bitr4i ⊢ ( ( ∃ 𝑥 ∈ 𝐴 𝜑 ∨ ∃ 𝑥 ∈ 𝐴 𝜓 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜓 ) )
8 1 3 7 3bitr4i ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∨ 𝜓 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∨ ∃ 𝑥 ∈ 𝐴 𝜓 ) )