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
|- ( ph <-> ps )
Assertion expandrex
|- ( E. x e. A ph <-> -. A. x ( x e. A -> -. ps ) )

Proof

Step Hyp Ref Expression
1 expandrex.1
 |-  ( ph <-> ps )
2 notnotb
 |-  ( ps <-> -. -. ps )
3 1 2 bitri
 |-  ( ph <-> -. -. ps )
4 3 expandrexn
 |-  ( E. x e. A ph <-> -. A. x ( x e. A -> -. ps ) )