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 ⊢ Ⅎ _ x B
riota2f.2 ⊢ Ⅎ x ψ
riota2f.3 ⊢ x = B → φ ↔ ψ
Assertion riota2f ⊢ B ∈ A ∧ ∃! x ∈ A φ → ψ ↔ ι x ∈ A | φ = B

Proof

Step Hyp Ref Expression
1 riota2f.1 ⊢ Ⅎ _ x B
2 riota2f.2 ⊢ Ⅎ x ψ
3 riota2f.3 ⊢ x = B → φ ↔ ψ
4 1 nfel1 ⊢ Ⅎ x B ∈ A
5 1 a1i ⊢ B ∈ A → Ⅎ _ x B
6 2 a1i ⊢ B ∈ A → Ⅎ x ψ
7 id ⊢ B ∈ A → B ∈ A
8 3 adantl ⊢ B ∈ A ∧ x = B → φ ↔ ψ
9 4 5 6 7 8 riota2df ⊢ B ∈ A ∧ ∃! x ∈ A φ → ψ ↔ ι x ∈ A | φ = B