Theorem iota2d

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	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
	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	⊢ ( 𝜑 → ( 𝜒 ↔ ( ℩ 𝑥 𝜓 ) = 𝐵 ) )