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

Metamath Proof Explorer

Theorem iota2d

Description: A condition that allows to represent "the unique element such that ph " with a class expression A . (Contributed by NM, 30-Dec-2014)

Ref Expression
Hypotheses iota2df.1 ⊢ φ → B ∈ V
iota2df.2 ⊢ φ → ∃! x ψ
iota2df.3 ⊢ φ ∧ x = B → ψ ↔ χ
Assertion iota2d ⊢ φ → χ ↔ ι x | ψ = B

Proof

Step Hyp Ref Expression
1 iota2df.1 ⊢ φ → B ∈ V
2 iota2df.2 ⊢ φ → ∃! x ψ
3 iota2df.3 ⊢ φ ∧ x = B → ψ ↔ χ
4 nfv ⊢ Ⅎ x φ
5 nfvd ⊢ φ → Ⅎ x χ
6 nfcvd ⊢ φ → Ⅎ _ x B
7 1 2 3 4 5 6 iota2df ⊢ φ → χ ↔ ι x | ψ = B