Metamath Proof Explorer

Theorem iota5f

Description: A method for computing iota. (Contributed by Scott Fenton, 13-Dec-2017)

Ref Expression
Hypotheses iota5f.1 ⊢ Ⅎ x φ
iota5f.2 ⊢ Ⅎ _ x A
iota5f.3 ⊢ φ ∧ A ∈ V → ψ ↔ x = A
Assertion iota5f ⊢ φ ∧ A ∈ V → ι x | ψ = A

Proof

Step Hyp Ref Expression
1 iota5f.1 ⊢ Ⅎ x φ
2 iota5f.2 ⊢ Ⅎ _ x A
3 iota5f.3 ⊢ φ ∧ A ∈ V → ψ ↔ x = A
4 2 nfel1 ⊢ Ⅎ x A ∈ V
5 1 4 nfan ⊢ Ⅎ x φ ∧ A ∈ V
6 5 3 alrimi ⊢ φ ∧ A ∈ V → ∀ x ψ ↔ x = A
7 2 nfeq2 ⊢ Ⅎ x y = A
8 eqeq2 ⊢ y = A → x = y ↔ x = A
9 8 bibi2d ⊢ y = A → ψ ↔ x = y ↔ ψ ↔ x = A
10 7 9 albid ⊢ y = A → ∀ x ψ ↔ x = y ↔ ∀ x ψ ↔ x = A
11 eqeq2 ⊢ y = A → ι x | ψ = y ↔ ι x | ψ = A
12 10 11 imbi12d ⊢ y = A → ∀ x ψ ↔ x = y → ι x | ψ = y ↔ ∀ x ψ ↔ x = A → ι x | ψ = A
13 iotaval ⊢ ∀ x ψ ↔ x = y → ι x | ψ = y
14 12 13 vtoclg ⊢ A ∈ V → ∀ x ψ ↔ x = A → ι x | ψ = A
15 14 adantl ⊢ φ ∧ A ∈ V → ∀ x ψ ↔ x = A → ι x | ψ = A
16 6 15 mpd ⊢ φ ∧ A ∈ V → ι x | ψ = A