2eu3

Description: Double existential uniqueness. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 3-Dec-2001) (Proof shortened by Wolf Lammen, 23-Apr-2023) (New usage is discouraged.)

		Ref	Expression
	Assertion	2eu3	⊢ ( ∀ 𝑥 ∀ 𝑦 ( ∃* 𝑥 𝜑 ∨ ∃* 𝑦 𝜑 ) → ( ( ∃! 𝑥 ∃! 𝑦 𝜑 ∧ ∃! 𝑦 ∃! 𝑥 𝜑 ) ↔ ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nfmo1	⊢ Ⅎ 𝑦 ∃* 𝑦 𝜑
2	1	19.31	⊢ ( ∀ 𝑦 ( ∃* 𝑥 𝜑 ∨ ∃* 𝑦 𝜑 ) ↔ ( ∀ 𝑦 ∃* 𝑥 𝜑 ∨ ∃* 𝑦 𝜑 ) )
3	2	albii	⊢ ( ∀ 𝑥 ∀ 𝑦 ( ∃* 𝑥 𝜑 ∨ ∃* 𝑦 𝜑 ) ↔ ∀ 𝑥 ( ∀ 𝑦 ∃* 𝑥 𝜑 ∨ ∃* 𝑦 𝜑 ) )
4		nfmo1	⊢ Ⅎ 𝑥 ∃* 𝑥 𝜑
5	4	nfal	⊢ Ⅎ 𝑥 ∀ 𝑦 ∃* 𝑥 𝜑
6	5	19.32	⊢ ( ∀ 𝑥 ( ∀ 𝑦 ∃* 𝑥 𝜑 ∨ ∃* 𝑦 𝜑 ) ↔ ( ∀ 𝑦 ∃* 𝑥 𝜑 ∨ ∀ 𝑥 ∃* 𝑦 𝜑 ) )
7	3 6	bitri	⊢ ( ∀ 𝑥 ∀ 𝑦 ( ∃* 𝑥 𝜑 ∨ ∃* 𝑦 𝜑 ) ↔ ( ∀ 𝑦 ∃* 𝑥 𝜑 ∨ ∀ 𝑥 ∃* 𝑦 𝜑 ) )
8		2eu1	⊢ ( ∀ 𝑦 ∃* 𝑥 𝜑 → ( ∃! 𝑦 ∃! 𝑥 𝜑 ↔ ( ∃! 𝑦 ∃ 𝑥 𝜑 ∧ ∃! 𝑥 ∃ 𝑦 𝜑 ) ) )
9	8	biimpd	⊢ ( ∀ 𝑦 ∃* 𝑥 𝜑 → ( ∃! 𝑦 ∃! 𝑥 𝜑 → ( ∃! 𝑦 ∃ 𝑥 𝜑 ∧ ∃! 𝑥 ∃ 𝑦 𝜑 ) ) )
10		ancom	⊢ ( ( ∃! 𝑦 ∃ 𝑥 𝜑 ∧ ∃! 𝑥 ∃ 𝑦 𝜑 ) ↔ ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) )
11	9 10	imbitrdi	⊢ ( ∀ 𝑦 ∃* 𝑥 𝜑 → ( ∃! 𝑦 ∃! 𝑥 𝜑 → ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) ) )
12		2eu1	⊢ ( ∀ 𝑥 ∃* 𝑦 𝜑 → ( ∃! 𝑥 ∃! 𝑦 𝜑 ↔ ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) ) )
13	12	biimpd	⊢ ( ∀ 𝑥 ∃* 𝑦 𝜑 → ( ∃! 𝑥 ∃! 𝑦 𝜑 → ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) ) )
14	11 13	jaoa	⊢ ( ( ∀ 𝑦 ∃* 𝑥 𝜑 ∨ ∀ 𝑥 ∃* 𝑦 𝜑 ) → ( ( ∃! 𝑦 ∃! 𝑥 𝜑 ∧ ∃! 𝑥 ∃! 𝑦 𝜑 ) → ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) ) )
15	14	ancomsd	⊢ ( ( ∀ 𝑦 ∃* 𝑥 𝜑 ∨ ∀ 𝑥 ∃* 𝑦 𝜑 ) → ( ( ∃! 𝑥 ∃! 𝑦 𝜑 ∧ ∃! 𝑦 ∃! 𝑥 𝜑 ) → ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) ) )
16		2exeu	⊢ ( ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) → ∃! 𝑥 ∃! 𝑦 𝜑 )
17		2exeu	⊢ ( ( ∃! 𝑦 ∃ 𝑥 𝜑 ∧ ∃! 𝑥 ∃ 𝑦 𝜑 ) → ∃! 𝑦 ∃! 𝑥 𝜑 )
18	17	ancoms	⊢ ( ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) → ∃! 𝑦 ∃! 𝑥 𝜑 )
19	16 18	jca	⊢ ( ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) → ( ∃! 𝑥 ∃! 𝑦 𝜑 ∧ ∃! 𝑦 ∃! 𝑥 𝜑 ) )
20	15 19	impbid1	⊢ ( ( ∀ 𝑦 ∃* 𝑥 𝜑 ∨ ∀ 𝑥 ∃* 𝑦 𝜑 ) → ( ( ∃! 𝑥 ∃! 𝑦 𝜑 ∧ ∃! 𝑦 ∃! 𝑥 𝜑 ) ↔ ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) ) )
21	7 20	sylbi	⊢ ( ∀ 𝑥 ∀ 𝑦 ( ∃* 𝑥 𝜑 ∨ ∃* 𝑦 𝜑 ) → ( ( ∃! 𝑥 ∃! 𝑦 𝜑 ∧ ∃! 𝑦 ∃! 𝑥 𝜑 ) ↔ ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) ) )

Metamath Proof Explorer

Theorem 2eu3

Proof