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

Metamath Proof Explorer

Theorem riota2

Description: This theorem shows a condition that allows to represent a descriptor with a class expression B . (Contributed by NM, 23-Aug-2011) (Revised by Mario Carneiro, 10-Dec-2016)

		Ref	Expression
	Hypothesis	riota2.1	⊢ ( 𝑥 = 𝐵 → ( 𝜑 ↔ 𝜓 ) )
	Assertion	riota2	⊢ ( ( 𝐵 ∈ 𝐴 ∧ ∃! 𝑥 ∈ 𝐴 𝜑 ) → ( 𝜓 ↔ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		riota2.1	⊢ ( 𝑥 = 𝐵 → ( 𝜑 ↔ 𝜓 ) )
2		nfcv	⊢ Ⅎ 𝑥 𝐵
3		nfv	⊢ Ⅎ 𝑥 𝜓
4	2 3 1	riota2f	⊢ ( ( 𝐵 ∈ 𝐴 ∧ ∃! 𝑥 ∈ 𝐴 𝜑 ) → ( 𝜓 ↔ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) = 𝐵 ) )