Metamath Proof Explorer


Theorem rexn0

Description: Restricted existential quantification implies its restriction is nonempty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007) Avoid df-clel , ax-8 . (Revised by Gino Giotto, 2-Sep-2024)

Ref Expression
Assertion rexn0 xAφA

Proof

Step Hyp Ref Expression
1 dfrex2 xAφ¬xA¬φ
2 rzal A=xA¬φ
3 2 con3i ¬xA¬φ¬A=
4 1 3 sylbi xAφ¬A=
5 4 neqned xAφA