Theorem modom

Description: Two ways to express "at most one". (Contributed by Stefan O'Rear, 28-Oct-2014)

	Ref	Expression
Assertion	modom	⊢ ( ∃* 𝑥 𝜑 ↔ { 𝑥 ∣ 𝜑 } ≼ 1o )

Proof

Step	Hyp	Ref	Expression
1		moeu	⊢ ( ∃* 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 → ∃! 𝑥 𝜑 ) )
2		imor	⊢ ( ( ∃ 𝑥 𝜑 → ∃! 𝑥 𝜑 ) ↔ ( ¬ ∃ 𝑥 𝜑 ∨ ∃! 𝑥 𝜑 ) )
3		abn0	⊢ ( { 𝑥 ∣ 𝜑 } ≠ ∅ ↔ ∃ 𝑥 𝜑 )
4	3	necon1bbii	⊢ ( ¬ ∃ 𝑥 𝜑 ↔ { 𝑥 ∣ 𝜑 } = ∅ )
5		sdom1	⊢ ( { 𝑥 ∣ 𝜑 } ≺ 1o ↔ { 𝑥 ∣ 𝜑 } = ∅ )
6	4 5	bitr4i	⊢ ( ¬ ∃ 𝑥 𝜑 ↔ { 𝑥 ∣ 𝜑 } ≺ 1o )
7		euen1	⊢ ( ∃! 𝑥 𝜑 ↔ { 𝑥 ∣ 𝜑 } ≈ 1o )
8	6 7	orbi12i	⊢ ( ( ¬ ∃ 𝑥 𝜑 ∨ ∃! 𝑥 𝜑 ) ↔ ( { 𝑥 ∣ 𝜑 } ≺ 1o ∨ { 𝑥 ∣ 𝜑 } ≈ 1o ) )
9		brdom2	⊢ ( { 𝑥 ∣ 𝜑 } ≼ 1o ↔ ( { 𝑥 ∣ 𝜑 } ≺ 1o ∨ { 𝑥 ∣ 𝜑 } ≈ 1o ) )
10	8 9	bitr4i	⊢ ( ( ¬ ∃ 𝑥 𝜑 ∨ ∃! 𝑥 𝜑 ) ↔ { 𝑥 ∣ 𝜑 } ≼ 1o )
11	1 2 10	3bitri	⊢ ( ∃* 𝑥 𝜑 ↔ { 𝑥 ∣ 𝜑 } ≼ 1o )