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 xAφ¬xxA¬ψ

Proof

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