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 ⊢ φ ∧ A ∈ V → ψ ↔ x = A
Assertion iota5 ⊢ φ ∧ A ∈ V → ι x | ψ = A

Proof

Step Hyp Ref Expression
1 iota5.1 ⊢ φ ∧ A ∈ V → ψ ↔ x = A
2 1 alrimiv ⊢ φ ∧ A ∈ V → ∀ x ψ ↔ x = A
3 eqeq2 ⊢ y = A → x = y ↔ x = A
4 3 bibi2d ⊢ y = A → ψ ↔ x = y ↔ ψ ↔ x = A
5 4 albidv ⊢ y = A → ∀ x ψ ↔ x = y ↔ ∀ x ψ ↔ x = A
6 eqeq2 ⊢ y = A → ι x | ψ = y ↔ ι x | ψ = A
7 5 6 imbi12d ⊢ y = A → ∀ x ψ ↔ x = y → ι x | ψ = y ↔ ∀ x ψ ↔ x = A → ι x | ψ = A
8 iotaval ⊢ ∀ x ψ ↔ x = y → ι x | ψ = y
9 7 8 vtoclg ⊢ A ∈ V → ∀ x ψ ↔ x = A → ι x | ψ = A
10 9 adantl ⊢ φ ∧ A ∈ V → ∀ x ψ ↔ x = A → ι x | ψ = A
11 2 10 mpd ⊢ φ ∧ A ∈ V → ι x | ψ = A