Theorem iota2

Description: The unique element such that ph . (Contributed by Jeff Madsen, 1-Jun-2011) (Revised by Mario Carneiro, 23-Dec-2016)

	Ref	Expression
Hypothesis	iota2.1	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
Assertion	iota2	⊢ ( ( 𝐴 ∈ 𝐵 ∧ ∃! 𝑥 𝜑 ) → ( 𝜓 ↔ ( ℩ 𝑥 𝜑 ) = 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		iota2.1	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
2		elex	⊢ ( 𝐴 ∈ 𝐵 → 𝐴 ∈ V )
3		simpl	⊢ ( ( 𝐴 ∈ V ∧ ∃! 𝑥 𝜑 ) → 𝐴 ∈ V )
4		simpr	⊢ ( ( 𝐴 ∈ V ∧ ∃! 𝑥 𝜑 ) → ∃! 𝑥 𝜑 )
5	1	adantl	⊢ ( ( ( 𝐴 ∈ V ∧ ∃! 𝑥 𝜑 ) ∧ 𝑥 = 𝐴 ) → ( 𝜑 ↔ 𝜓 ) )
6		nfv	⊢ Ⅎ 𝑥 𝐴 ∈ V
7		nfeu1	⊢ Ⅎ 𝑥 ∃! 𝑥 𝜑
8	6 7	nfan	⊢ Ⅎ 𝑥 ( 𝐴 ∈ V ∧ ∃! 𝑥 𝜑 )
9		nfvd	⊢ ( ( 𝐴 ∈ V ∧ ∃! 𝑥 𝜑 ) → Ⅎ 𝑥 𝜓 )
10		nfcvd	⊢ ( ( 𝐴 ∈ V ∧ ∃! 𝑥 𝜑 ) → Ⅎ 𝑥 𝐴 )
11	3 4 5 8 9 10	iota2df	⊢ ( ( 𝐴 ∈ V ∧ ∃! 𝑥 𝜑 ) → ( 𝜓 ↔ ( ℩ 𝑥 𝜑 ) = 𝐴 ) )
12	2 11	sylan	⊢ ( ( 𝐴 ∈ 𝐵 ∧ ∃! 𝑥 𝜑 ) → ( 𝜓 ↔ ( ℩ 𝑥 𝜑 ) = 𝐴 ) )