Theorem 2sb8e

Description: An equivalent expression for double existence. Usage of this theorem is discouraged because it depends on ax-13 . For a version requiring more disjoint variables, but fewer axioms, see 2sb8ev . (Contributed by Wolf Lammen, 2-Nov-2019) (New usage is discouraged.)

	Ref	Expression
Assertion	2sb8e	⊢ ( ∃ 𝑥 ∃ 𝑦 𝜑 ↔ ∃ 𝑧 ∃ 𝑤 [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		nfv	⊢ Ⅎ 𝑤 𝜑
2	1	sb8e	⊢ ( ∃ 𝑦 𝜑 ↔ ∃ 𝑤 [ 𝑤 / 𝑦 ] 𝜑 )
3	2	exbii	⊢ ( ∃ 𝑥 ∃ 𝑦 𝜑 ↔ ∃ 𝑥 ∃ 𝑤 [ 𝑤 / 𝑦 ] 𝜑 )
4		excom	⊢ ( ∃ 𝑥 ∃ 𝑤 [ 𝑤 / 𝑦 ] 𝜑 ↔ ∃ 𝑤 ∃ 𝑥 [ 𝑤 / 𝑦 ] 𝜑 )
5	3 4	bitri	⊢ ( ∃ 𝑥 ∃ 𝑦 𝜑 ↔ ∃ 𝑤 ∃ 𝑥 [ 𝑤 / 𝑦 ] 𝜑 )
6		nfv	⊢ Ⅎ 𝑧 𝜑
7	6	nfsb	⊢ Ⅎ 𝑧 [ 𝑤 / 𝑦 ] 𝜑
8	7	sb8e	⊢ ( ∃ 𝑥 [ 𝑤 / 𝑦 ] 𝜑 ↔ ∃ 𝑧 [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )
9	8	exbii	⊢ ( ∃ 𝑤 ∃ 𝑥 [ 𝑤 / 𝑦 ] 𝜑 ↔ ∃ 𝑤 ∃ 𝑧 [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )
10		excom	⊢ ( ∃ 𝑤 ∃ 𝑧 [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ ∃ 𝑧 ∃ 𝑤 [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )
11	5 9 10	3bitri	⊢ ( ∃ 𝑥 ∃ 𝑦 𝜑 ↔ ∃ 𝑧 ∃ 𝑤 [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )