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

Metamath Proof Explorer

Theorem iota5

Description: A method for computing iota. (Contributed by NM, 17-Sep-2013)

Ref Expression
Hypothesis iota5.1 ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → ( 𝜓 ↔ 𝑥 = 𝐴 ) )
Assertion iota5 ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → ( ℩ 𝑥 𝜓 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 iota5.1 ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → ( 𝜓 ↔ 𝑥 = 𝐴 ) )
2 1 alrimiv ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝐴 ) )
3 eqeq2 ⊢ ( 𝑦 = 𝐴 → ( 𝑥 = 𝑦 ↔ 𝑥 = 𝐴 ) )
4 3 bibi2d ⊢ ( 𝑦 = 𝐴 → ( ( 𝜓 ↔ 𝑥 = 𝑦 ) ↔ ( 𝜓 ↔ 𝑥 = 𝐴 ) ) )
5 4 albidv ⊢ ( 𝑦 = 𝐴 → ( ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝐴 ) ) )
6 eqeq2 ⊢ ( 𝑦 = 𝐴 → ( ( ℩ 𝑥 𝜓 ) = 𝑦 ↔ ( ℩ 𝑥 𝜓 ) = 𝐴 ) )
7 5 6 imbi12d ⊢ ( 𝑦 = 𝐴 → ( ( ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝑦 ) → ( ℩ 𝑥 𝜓 ) = 𝑦 ) ↔ ( ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝐴 ) → ( ℩ 𝑥 𝜓 ) = 𝐴 ) ) )
8 iotaval ⊢ ( ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝑦 ) → ( ℩ 𝑥 𝜓 ) = 𝑦 )
9 7 8 vtoclg ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝐴 ) → ( ℩ 𝑥 𝜓 ) = 𝐴 ) )
10 9 adantl ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → ( ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝐴 ) → ( ℩ 𝑥 𝜓 ) = 𝐴 ) )
11 2 10 mpd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → ( ℩ 𝑥 𝜓 ) = 𝐴 )