Theorem riotaund

Description: Restricted iota equals the empty set when not meaningful. (Contributed by NM, 16-Jan-2012) (Revised by Mario Carneiro, 15-Oct-2016) (Revised by NM, 13-Sep-2018)

	Ref	Expression
Assertion	riotaund	⊢ ( ¬ ∃! 𝑥 ∈ 𝐴 𝜑 → ( ℩ 𝑥 ∈ 𝐴 𝜑 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		df-riota	⊢ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) = ( ℩ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
2		df-reu	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
3		iotanul	⊢ ( ¬ ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → ( ℩ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) = ∅ )
4	2 3	sylnbi	⊢ ( ¬ ∃! 𝑥 ∈ 𝐴 𝜑 → ( ℩ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) = ∅ )
5	1 4	syl5eq	⊢ ( ¬ ∃! 𝑥 ∈ 𝐴 𝜑 → ( ℩ 𝑥 ∈ 𝐴 𝜑 ) = ∅ )