This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-riota

Description: Define restricted description binder. In case there is no unique x such that ( x e. A /\ ph ) holds, it evaluates to the empty set. See also comments for df-iota . (Contributed by NM, 15-Sep-2011) (Revised by Mario Carneiro, 15-Oct-2016) (Revised by NM, 2-Sep-2018)

		Ref	Expression
	Assertion	df-riota	⊢ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) = ( ℩ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	⊢ 𝑥
1		cA	⊢ 𝐴
2		wph	⊢ 𝜑
3	2 0 1	crio	⊢ ( ℩ 𝑥 ∈ 𝐴 𝜑 )
4	0	cv	⊢ 𝑥
5	4 1	wcel	⊢ 𝑥 ∈ 𝐴
6	5 2	wa	⊢ ( 𝑥 ∈ 𝐴 ∧ 𝜑 )
7	6 0	cio	⊢ ( ℩ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
8	3 7	wceq	⊢ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) = ( ℩ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )