Theorem 2exanali

Description: Theorem *11.521 in WhiteheadRussell p. 164. (Contributed by Andrew Salmon, 24-May-2011)

	Ref	Expression
Assertion	2exanali	⊢ ( ¬ ∃ 𝑥 ∃ 𝑦 ( 𝜑 ∧ ¬ 𝜓 ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝜑 → 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		2nalexn	⊢ ( ¬ ∀ 𝑥 ∀ 𝑦 ( 𝜑 → 𝜓 ) ↔ ∃ 𝑥 ∃ 𝑦 ¬ ( 𝜑 → 𝜓 ) )
2	1	con1bii	⊢ ( ¬ ∃ 𝑥 ∃ 𝑦 ¬ ( 𝜑 → 𝜓 ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝜑 → 𝜓 ) )
3		annim	⊢ ( ( 𝜑 ∧ ¬ 𝜓 ) ↔ ¬ ( 𝜑 → 𝜓 ) )
4	3	2exbii	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝜑 ∧ ¬ 𝜓 ) ↔ ∃ 𝑥 ∃ 𝑦 ¬ ( 𝜑 → 𝜓 ) )
5	2 4	xchnxbir	⊢ ( ¬ ∃ 𝑥 ∃ 𝑦 ( 𝜑 ∧ ¬ 𝜓 ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝜑 → 𝜓 ) )