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

Proof

Step Hyp Ref Expression
1 expandrexn.1 ( 𝜑 ↔ ¬ 𝜓 )
2 1 rexbii ( ∃ 𝑥𝐴 𝜑 ↔ ∃ 𝑥𝐴 ¬ 𝜓 )
3 df-rex ( ∃ 𝑥𝐴 ¬ 𝜓 ↔ ∃ 𝑥 ( 𝑥𝐴 ∧ ¬ 𝜓 ) )
4 exanali ( ∃ 𝑥 ( 𝑥𝐴 ∧ ¬ 𝜓 ) ↔ ¬ ∀ 𝑥 ( 𝑥𝐴𝜓 ) )
5 2 3 4 3bitri ( ∃ 𝑥𝐴 𝜑 ↔ ¬ ∀ 𝑥 ( 𝑥𝐴𝜓 ) )