Metamath Proof Explorer


Theorem rexanali

Description: A transformation of restricted quantifiers and logical connectives. (Contributed by NM, 4-Sep-2005) (Proof shortened by Wolf Lammen, 27-Dec-2019)

Ref Expression
Assertion rexanali
|- ( E. x e. A ( ph /\ -. ps ) <-> -. A. x e. A ( ph -> ps ) )

Proof

Step Hyp Ref Expression
1 dfrex2
 |-  ( E. x e. A ( ph /\ -. ps ) <-> -. A. x e. A -. ( ph /\ -. ps ) )
2 iman
 |-  ( ( ph -> ps ) <-> -. ( ph /\ -. ps ) )
3 2 ralbii
 |-  ( A. x e. A ( ph -> ps ) <-> A. x e. A -. ( ph /\ -. ps ) )
4 1 3 xchbinxr
 |-  ( E. x e. A ( ph /\ -. ps ) <-> -. A. x e. A ( ph -> ps ) )