This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 2sb8ef

Description: An equivalent expression for double existence. Version of 2sb8e with more disjoint variable conditions, not requiring ax-13 . (Contributed by Wolf Lammen, 28-Jan-2023)

		Ref	Expression
	Hypotheses	2sb8ef.1	⊢ Ⅎ 𝑤 𝜑
		2sb8ef.2	⊢ Ⅎ 𝑧 𝜑
	Assertion	2sb8ef	⊢ ( ∃ 𝑥 ∃ 𝑦 𝜑 ↔ ∃ 𝑧 ∃ 𝑤 [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )

Proof

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