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

Metamath Proof Explorer

Theorem riotaprop

Description: Properties of a restricted definite description operator. (Contributed by NM, 23-Nov-2013)

Ref Expression
Hypotheses riotaprop.0 ⊢ Ⅎ x ψ
riotaprop.1 ⊢ B = ι x ∈ A | φ
riotaprop.2 ⊢ x = B → φ ↔ ψ
Assertion riotaprop ⊢ ∃! x ∈ A φ → B ∈ A ∧ ψ

Proof

Step Hyp Ref Expression
1 riotaprop.0 ⊢ Ⅎ x ψ
2 riotaprop.1 ⊢ B = ι x ∈ A | φ
3 riotaprop.2 ⊢ x = B → φ ↔ ψ
4 riotacl ⊢ ∃! x ∈ A φ → ι x ∈ A | φ ∈ A
5 2 4 eqeltrid ⊢ ∃! x ∈ A φ → B ∈ A
6 2 eqcomi ⊢ ι x ∈ A | φ = B
7 nfriota1 ⊢ Ⅎ _ x ι x ∈ A | φ
8 2 7 nfcxfr ⊢ Ⅎ _ x B
9 8 1 3 riota2f ⊢ B ∈ A ∧ ∃! x ∈ A φ → ψ ↔ ι x ∈ A | φ = B
10 6 9 mpbiri ⊢ B ∈ A ∧ ∃! x ∈ A φ → ψ
11 5 10 mpancom ⊢ ∃! x ∈ A φ → ψ
12 5 11 jca ⊢ ∃! x ∈ A φ → B ∈ A ∧ ψ