Metamath Proof Explorer


Theorem rexim

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 x A φ ψ x A φ x A ψ

Proof

Step Hyp Ref Expression
1 con3 φ ψ ¬ ψ ¬ φ
2 1 ral2imi x A φ ψ x A ¬ ψ x A ¬ φ
3 2 con3d x A φ ψ ¬ x A ¬ φ ¬ x A ¬ ψ
4 dfrex2 x A φ ¬ x A ¬ φ
5 dfrex2 x A ψ ¬ x A ¬ ψ
6 3 4 5 3imtr4g x A φ ψ x A φ x A ψ