Metamath Proof Explorer


Theorem rexnal2

Description: Relationship between two restricted universal and existential quantifiers. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion rexnal2 xAyB¬φ¬xAyBφ

Proof

Step Hyp Ref Expression
1 rexnal yB¬φ¬yBφ
2 1 rexbii xAyB¬φxA¬yBφ
3 rexnal xA¬yBφ¬xAyBφ
4 2 3 bitri xAyB¬φ¬xAyBφ