Description: Theorem *11.51 in WhiteheadRussell p. 164. (Contributed by Andrew Salmon, 24-May-2011) (Proof shortened by Wolf Lammen, 25-Sep-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | 2exnexn | |- ( E. x A. y ph <-> -. A. x E. y -. ph ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alexn | |- ( A. x E. y -. ph <-> -. E. x A. y ph ) |
|
2 | 1 | con2bii | |- ( E. x A. y ph <-> -. A. x E. y -. ph ) |