Theorem 2mo2

Description: Two ways of expressing "there exists at most one ordered pair <. x , y >. such that ph ( x , y ) holds. Note that this is not equivalent to E* x E* y ph . See also 2mo . This is the analogue of 2eu4 for existential uniqueness. (Contributed by Wolf Lammen, 26-Oct-2019) Reduce dependencies on axioms. (Revised by Wolf Lammen, 3-Jan-2023)

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

Proof

Step	Hyp	Ref	Expression
1		exdistrv	⊢ ( ∃ 𝑧 ∃ 𝑤 ( ∀ 𝑥 ( ∃ 𝑦 𝜑 → 𝑥 = 𝑧 ) ∧ ∀ 𝑦 ( ∃ 𝑥 𝜑 → 𝑦 = 𝑤 ) ) ↔ ( ∃ 𝑧 ∀ 𝑥 ( ∃ 𝑦 𝜑 → 𝑥 = 𝑧 ) ∧ ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑥 𝜑 → 𝑦 = 𝑤 ) ) )
2		jcab	⊢ ( ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ( ( 𝜑 → 𝑥 = 𝑧 ) ∧ ( 𝜑 → 𝑦 = 𝑤 ) ) )
3	2	2albii	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 → 𝑥 = 𝑧 ) ∧ ( 𝜑 → 𝑦 = 𝑤 ) ) )
4		19.26-2	⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 → 𝑥 = 𝑧 ) ∧ ( 𝜑 → 𝑦 = 𝑤 ) ) ↔ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → 𝑥 = 𝑧 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝜑 → 𝑦 = 𝑤 ) ) )
5		19.23v	⊢ ( ∀ 𝑦 ( 𝜑 → 𝑥 = 𝑧 ) ↔ ( ∃ 𝑦 𝜑 → 𝑥 = 𝑧 ) )
6	5	albii	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → 𝑥 = 𝑧 ) ↔ ∀ 𝑥 ( ∃ 𝑦 𝜑 → 𝑥 = 𝑧 ) )
7		alcom	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → 𝑦 = 𝑤 ) ↔ ∀ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑦 = 𝑤 ) )
8		19.23v	⊢ ( ∀ 𝑥 ( 𝜑 → 𝑦 = 𝑤 ) ↔ ( ∃ 𝑥 𝜑 → 𝑦 = 𝑤 ) )
9	8	albii	⊢ ( ∀ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑦 = 𝑤 ) ↔ ∀ 𝑦 ( ∃ 𝑥 𝜑 → 𝑦 = 𝑤 ) )
10	7 9	bitri	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → 𝑦 = 𝑤 ) ↔ ∀ 𝑦 ( ∃ 𝑥 𝜑 → 𝑦 = 𝑤 ) )
11	6 10	anbi12i	⊢ ( ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → 𝑥 = 𝑧 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝜑 → 𝑦 = 𝑤 ) ) ↔ ( ∀ 𝑥 ( ∃ 𝑦 𝜑 → 𝑥 = 𝑧 ) ∧ ∀ 𝑦 ( ∃ 𝑥 𝜑 → 𝑦 = 𝑤 ) ) )
12	3 4 11	3bitri	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ( ∀ 𝑥 ( ∃ 𝑦 𝜑 → 𝑥 = 𝑧 ) ∧ ∀ 𝑦 ( ∃ 𝑥 𝜑 → 𝑦 = 𝑤 ) ) )
13	12	2exbii	⊢ ( ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ∃ 𝑧 ∃ 𝑤 ( ∀ 𝑥 ( ∃ 𝑦 𝜑 → 𝑥 = 𝑧 ) ∧ ∀ 𝑦 ( ∃ 𝑥 𝜑 → 𝑦 = 𝑤 ) ) )
14		df-mo	⊢ ( ∃* 𝑥 ∃ 𝑦 𝜑 ↔ ∃ 𝑧 ∀ 𝑥 ( ∃ 𝑦 𝜑 → 𝑥 = 𝑧 ) )
15		df-mo	⊢ ( ∃* 𝑦 ∃ 𝑥 𝜑 ↔ ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑥 𝜑 → 𝑦 = 𝑤 ) )
16	14 15	anbi12i	⊢ ( ( ∃* 𝑥 ∃ 𝑦 𝜑 ∧ ∃* 𝑦 ∃ 𝑥 𝜑 ) ↔ ( ∃ 𝑧 ∀ 𝑥 ( ∃ 𝑦 𝜑 → 𝑥 = 𝑧 ) ∧ ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑥 𝜑 → 𝑦 = 𝑤 ) ) )
17	1 13 16	3bitr4ri	⊢ ( ( ∃* 𝑥 ∃ 𝑦 𝜑 ∧ ∃* 𝑦 ∃ 𝑥 𝜑 ) ↔ ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )