Metamath Proof Explorer


Theorem expandrexn

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

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

Proof

Step Hyp Ref Expression
1 expandrexn.1 φ ¬ ψ
2 1 rexbii x A φ x A ¬ ψ
3 df-rex x A ¬ ψ x x A ¬ ψ
4 exanali x x A ¬ ψ ¬ x x A ψ
5 2 3 4 3bitri x A φ ¬ x x A ψ