Metamath Proof Explorer


Theorem expandrex

Description: Expand a restricted existential quantifier to primitives. (Contributed by Rohan Ridenour, 13-Aug-2023)

Ref Expression
Hypothesis expandrex.1 φ ψ
Assertion expandrex x A φ ¬ x x A ¬ ψ

Proof

Step Hyp Ref Expression
1 expandrex.1 φ ψ
2 notnotb ψ ¬ ¬ ψ
3 1 2 bitri φ ¬ ¬ ψ
4 3 expandrexn x A φ ¬ x x A ¬ ψ