Description: Theorem 19.22 of Margaris p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994) (Proof shortened by Andrew Salmon, 30-May-2011)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | rexim | ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) → ( ∃ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜓 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | con3 | ⊢ ( ( 𝜑 → 𝜓 ) → ( ¬ 𝜓 → ¬ 𝜑 ) ) | |
| 2 | 1 | ral2imi | ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) → ( ∀ 𝑥 ∈ 𝐴 ¬ 𝜓 → ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 ) ) |
| 3 | 2 | con3d | ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) → ( ¬ ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 → ¬ ∀ 𝑥 ∈ 𝐴 ¬ 𝜓 ) ) |
| 4 | dfrex2 | ⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 ) | |
| 5 | dfrex2 | ⊢ ( ∃ 𝑥 ∈ 𝐴 𝜓 ↔ ¬ ∀ 𝑥 ∈ 𝐴 ¬ 𝜓 ) | |
| 6 | 3 4 5 | 3imtr4g | ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) → ( ∃ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜓 ) ) |