Metamath Proof Explorer

Theorem iotaval

Description: Theorem 8.19 in Quine p. 57. This theorem is the fundamental property of iota. (Contributed by Andrew Salmon, 11-Jul-2011)

Ref Expression
Assertion iotaval ⊢ ∀ x φ ↔ x = y → ι x | φ = y

Proof

Step Hyp Ref Expression
1 dfiota2 ⊢ ι x | φ = ⋃ z | ∀ x φ ↔ x = z
2 sbeqalb ⊢ y ∈ V → ∀ x φ ↔ x = y ∧ ∀ x φ ↔ x = z → y = z
3 2 elv ⊢ ∀ x φ ↔ x = y ∧ ∀ x φ ↔ x = z → y = z
4 3 ex ⊢ ∀ x φ ↔ x = y → ∀ x φ ↔ x = z → y = z
5 equequ2 ⊢ y = z → x = y ↔ x = z
6 5 bibi2d ⊢ y = z → φ ↔ x = y ↔ φ ↔ x = z
7 6 biimpd ⊢ y = z → φ ↔ x = y → φ ↔ x = z
8 7 alimdv ⊢ y = z → ∀ x φ ↔ x = y → ∀ x φ ↔ x = z
9 8 com12 ⊢ ∀ x φ ↔ x = y → y = z → ∀ x φ ↔ x = z
10 4 9 impbid ⊢ ∀ x φ ↔ x = y → ∀ x φ ↔ x = z ↔ y = z
11 equcom ⊢ y = z ↔ z = y
12 10 11 syl6bb ⊢ ∀ x φ ↔ x = y → ∀ x φ ↔ x = z ↔ z = y
13 12 alrimiv ⊢ ∀ x φ ↔ x = y → ∀ z ∀ x φ ↔ x = z ↔ z = y
14 uniabio ⊢ ∀ z ∀ x φ ↔ x = z ↔ z = y → ⋃ z | ∀ x φ ↔ x = z = y
15 13 14 syl ⊢ ∀ x φ ↔ x = y → ⋃ z | ∀ x φ ↔ x = z = y
16 1 15 syl5eq ⊢ ∀ x φ ↔ x = y → ι x | φ = y