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 ( ∃ 𝑥𝐴 𝜑 ↔ ¬ ∀ 𝑥 ( 𝑥𝐴 → ¬ 𝜓 ) )

Proof

Step Hyp Ref Expression
1 expandrex.1 ( 𝜑𝜓 )
2 notnotb ( 𝜓 ↔ ¬ ¬ 𝜓 )
3 1 2 bitri ( 𝜑 ↔ ¬ ¬ 𝜓 )
4 3 expandrexn ( ∃ 𝑥𝐴 𝜑 ↔ ¬ ∀ 𝑥 ( 𝑥𝐴 → ¬ 𝜓 ) )