Metamath Proof Explorer


Theorem iota2df

Description: A condition that allows us 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