Metamath Proof Explorer


Theorem rexsng

Description: Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012) Avoid ax-10 , ax-12 . (Revised by Gino Giotto, 30-Sep-2024)

Ref Expression
Hypothesis ralsng.1 x = A φ ψ
Assertion rexsng A V x A φ ψ

Proof

Step Hyp Ref Expression
1 ralsng.1 x = A φ ψ
2 1 notbid x = A ¬ φ ¬ ψ
3 2 ralsng A V x A ¬ φ ¬ ψ
4 dfrex2 x A φ ¬ x A ¬ φ
5 bicom1 x A ¬ φ ¬ ψ ¬ ψ x A ¬ φ
6 5 con1bid x A ¬ φ ¬ ψ ¬ x A ¬ φ ψ
7 4 6 bitrid x A ¬ φ ¬ ψ x A φ ψ
8 3 7 syl A V x A φ ψ