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