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

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 ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
iota2df.2 ⊢ ( 𝜑 → ∃! 𝑥 𝜓 )
iota2df.3 ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐵 ) → ( 𝜓 ↔ 𝜒 ) )
iota2df.4 ⊢ Ⅎ 𝑥 𝜑
iota2df.5 ⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
iota2df.6 ⊢ ( 𝜑 → Ⅎ 𝑥 𝐵 )
Assertion iota2df ( 𝜑 → ( 𝜒 ↔ ( ℩ 𝑥 𝜓 ) = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 iota2df.1 ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
2 iota2df.2 ⊢ ( 𝜑 → ∃! 𝑥 𝜓 )
3 iota2df.3 ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐵 ) → ( 𝜓 ↔ 𝜒 ) )
4 iota2df.4 ⊢ Ⅎ 𝑥 𝜑
5 iota2df.5 ⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
6 iota2df.6 ⊢ ( 𝜑 → Ⅎ 𝑥 𝐵 )
7 simpr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐵 ) → 𝑥 = 𝐵 )
8 7 eqeq2d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐵 ) → ( ( ℩ 𝑥 𝜓 ) = 𝑥 ↔ ( ℩ 𝑥 𝜓 ) = 𝐵 ) )
9 3 8 bibi12d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐵 ) → ( ( 𝜓 ↔ ( ℩ 𝑥 𝜓 ) = 𝑥 ) ↔ ( 𝜒 ↔ ( ℩ 𝑥 𝜓 ) = 𝐵 ) ) )
10 iota1 ⊢ ( ∃! 𝑥 𝜓 → ( 𝜓 ↔ ( ℩ 𝑥 𝜓 ) = 𝑥 ) )
11 2 10 syl ⊢ ( 𝜑 → ( 𝜓 ↔ ( ℩ 𝑥 𝜓 ) = 𝑥 ) )
12 nfiota1 ⊢ Ⅎ 𝑥 ( ℩ 𝑥 𝜓 )
13 12 a1i ⊢ ( 𝜑 → Ⅎ 𝑥 ( ℩ 𝑥 𝜓 ) )
14 13 6 nfeqd ⊢ ( 𝜑 → Ⅎ 𝑥 ( ℩ 𝑥 𝜓 ) = 𝐵 )
15 5 14 nfbid ⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝜒 ↔ ( ℩ 𝑥 𝜓 ) = 𝐵 ) )
16 1 9 11 4 6 15 vtocldf ⊢ ( 𝜑 → ( 𝜒 ↔ ( ℩ 𝑥 𝜓 ) = 𝐵 ) )