Metamath Proof Explorer


Theorem dfral2

Description: Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997) Allow shortening of rexnal . (Revised by Wolf Lammen, 9-Dec-2019)

Ref Expression
Assertion dfral2 xAφ¬xA¬φ

Proof

Step Hyp Ref Expression
1 notnotb φ¬¬φ
2 1 ralbii xAφxA¬¬φ
3 ralnex xA¬¬φ¬xA¬φ
4 2 3 bitri xAφ¬xA¬φ