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 ) ) |
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 ) ) |