Theorem 2exsb

Description: An equivalent expression for double existence. (Contributed by NM, 2-Feb-2005) (Proof shortened by Wolf Lammen, 30-Sep-2018)

	Ref	Expression
Assertion	2exsb	⊢ ( ∃ 𝑥 ∃ 𝑦 𝜑 ↔ ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		nfv	⊢ Ⅎ 𝑤 𝜑
2		nfv	⊢ Ⅎ 𝑧 𝜑
3	1 2	2sb8ev	⊢ ( ∃ 𝑥 ∃ 𝑦 𝜑 ↔ ∃ 𝑧 ∃ 𝑤 [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )
4		2sb6	⊢ ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝜑 ) )
5	4	2exbii	⊢ ( ∃ 𝑧 ∃ 𝑤 [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝜑 ) )
6	3 5	bitri	⊢ ( ∃ 𝑥 ∃ 𝑦 𝜑 ↔ ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝜑 ) )