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

Metamath Proof Explorer

Theorem rexlimd3

Description: * Inference from Theorem 19.23 of Margaris p. 90 (restricted quantifier version). (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses rexlimd3.1 ⊢ Ⅎ x φ
rexlimd3.2 ⊢ Ⅎ x χ
rexlimd3.3 ⊢ φ ∧ x ∈ A ∧ ψ → χ
Assertion rexlimd3 ⊢ φ → ∃ x ∈ A ψ → χ

Proof

Step Hyp Ref Expression
1 rexlimd3.1 ⊢ Ⅎ x φ
2 rexlimd3.2 ⊢ Ⅎ x χ
3 rexlimd3.3 ⊢ φ ∧ x ∈ A ∧ ψ → χ
4 3 exp31 ⊢ φ → x ∈ A → ψ → χ
5 1 2 4 rexlimd ⊢ φ → ∃ x ∈ A ψ → χ