Metamath Proof Explorer

Theorem iota2df

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 → ψ ↔ χ
iota2df.4 ⊢ Ⅎ x φ
iota2df.5 ⊢ φ → Ⅎ x χ
iota2df.6 ⊢ φ → Ⅎ _ x B
Assertion iota2df ⊢ φ → χ ↔ ι x | ψ = B

Proof

Step Hyp Ref Expression
1 iota2df.1 ⊢ φ → B ∈ V
2 iota2df.2 ⊢ φ → ∃! x ψ
3 iota2df.3 ⊢ φ ∧ x = B → ψ ↔ χ
4 iota2df.4 ⊢ Ⅎ x φ
5 iota2df.5 ⊢ φ → Ⅎ x χ
6 iota2df.6 ⊢ φ → Ⅎ _ x B
7 simpr ⊢ φ ∧ x = B → x = B
8 7 eqeq2d ⊢ φ ∧ x = B → ι x | ψ = x ↔ ι x | ψ = B
9 3 8 bibi12d ⊢ φ ∧ x = B → ψ ↔ ι x | ψ = x ↔ χ ↔ ι x | ψ = B
10 iota1 ⊢ ∃! x ψ → ψ ↔ ι x | ψ = x
11 2 10 syl ⊢ φ → ψ ↔ ι x | ψ = x
12 nfiota1 ⊢ Ⅎ _ x ι x | ψ
13 12 a1i ⊢ φ → Ⅎ _ x ι x | ψ
14 13 6 nfeqd ⊢ φ → Ⅎ x ι x | ψ = B
15 5 14 nfbid ⊢ φ → Ⅎ x χ ↔ ι x | ψ = B
16 1 9 11 4 6 15 vtocldf ⊢ φ → χ ↔ ι x | ψ = B