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

Proof

Step Hyp Ref Expression
1 iota2df.1 ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
2 iota2df.2 ⊢ ( 𝜑 → ∃! 𝑥 𝜓 )
3 iota2df.3 ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐵 ) → ( 𝜓 ↔ 𝜒 ) )
4 nfv ⊢ Ⅎ 𝑥 𝜑
5 nfvd ⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
6 nfcvd ⊢ ( 𝜑 → Ⅎ 𝑥 𝐵 )
7 1 2 3 4 5 6 iota2df ⊢ ( 𝜑 → ( 𝜒 ↔ ( ℩ 𝑥 𝜓 ) = 𝐵 ) )