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

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 ∈ 𝐵 ∧ ∃! 𝑥 𝜑 ) → ( 𝜓 ↔ ( ℩ 𝑥 𝜑 ) = 𝐴 ) )