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

Metamath Proof Explorer

Theorem riota2f

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, 15-Oct-2016)

Ref Expression
Hypotheses riota2f.1 ⊢ Ⅎ 𝑥 𝐵
riota2f.2 ⊢ Ⅎ 𝑥 𝜓
riota2f.3 ⊢ ( 𝑥 = 𝐵 → ( 𝜑 ↔ 𝜓 ) )
Assertion riota2f ( ( 𝐵 ∈ 𝐴 ∧ ∃! 𝑥 ∈ 𝐴 𝜑 ) → ( 𝜓 ↔ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 riota2f.1 ⊢ Ⅎ 𝑥 𝐵
2 riota2f.2 ⊢ Ⅎ 𝑥 𝜓
3 riota2f.3 ⊢ ( 𝑥 = 𝐵 → ( 𝜑 ↔ 𝜓 ) )
4 1 nfel1 ⊢ Ⅎ 𝑥 𝐵 ∈ 𝐴
5 1 a1i ⊢ ( 𝐵 ∈ 𝐴 → Ⅎ 𝑥 𝐵 )
6 2 a1i ⊢ ( 𝐵 ∈ 𝐴 → Ⅎ 𝑥 𝜓 )
7 id ⊢ ( 𝐵 ∈ 𝐴 → 𝐵 ∈ 𝐴 )
8 3 adantl ⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝑥 = 𝐵 ) → ( 𝜑 ↔ 𝜓 ) )
9 4 5 6 7 8 riota2df ⊢ ( ( 𝐵 ∈ 𝐴 ∧ ∃! 𝑥 ∈ 𝐴 𝜑 ) → ( 𝜓 ↔ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) = 𝐵 ) )