Theorem 2eu5OLD

Description: Obsolete version of 2eu5 as of 2-Oct-2023. (Contributed by NM, 26-Oct-2003) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		2eu1	⊢ ( ∀ 𝑥 ∃* 𝑦 𝜑 → ( ∃! 𝑥 ∃! 𝑦 𝜑 ↔ ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) ) )
2	1	pm5.32ri	⊢ ( ( ∃! 𝑥 ∃! 𝑦 𝜑 ∧ ∀ 𝑥 ∃* 𝑦 𝜑 ) ↔ ( ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) ∧ ∀ 𝑥 ∃* 𝑦 𝜑 ) )
3		eumo	⊢ ( ∃! 𝑦 ∃ 𝑥 𝜑 → ∃* 𝑦 ∃ 𝑥 𝜑 )
4	3	adantl	⊢ ( ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) → ∃* 𝑦 ∃ 𝑥 𝜑 )
5		2moex	⊢ ( ∃* 𝑦 ∃ 𝑥 𝜑 → ∀ 𝑥 ∃* 𝑦 𝜑 )
6	4 5	syl	⊢ ( ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) → ∀ 𝑥 ∃* 𝑦 𝜑 )
7	6	pm4.71i	⊢ ( ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) ↔ ( ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) ∧ ∀ 𝑥 ∃* 𝑦 𝜑 ) )
8		2eu4	⊢ ( ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) ↔ ( ∃ 𝑥 ∃ 𝑦 𝜑 ∧ ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )
9	2 7 8	3bitr2i	⊢ ( ( ∃! 𝑥 ∃! 𝑦 𝜑 ∧ ∀ 𝑥 ∃* 𝑦 𝜑 ) ↔ ( ∃ 𝑥 ∃ 𝑦 𝜑 ∧ ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )