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

Metamath Proof Explorer

Theorem iotavalb

Description: Theorem *14.202 in WhiteheadRussell p. 189. A biconditional version of iotaval . (Contributed by Andrew Salmon, 11-Jul-2011)

Ref Expression
Assertion iotavalb ⊢ ∃! x φ → ∀ x φ ↔ x = y ↔ ι x | φ = y

Proof

Step Hyp Ref Expression
1 iotaval ⊢ ∀ x φ ↔ x = y → ι x | φ = y
2 iotasbc ⊢ ∃! x φ → [˙ ι x | φ / z]˙ z = y ↔ ∃ z ∀ x φ ↔ x = z ∧ z = y
3 iotaexeu ⊢ ∃! x φ → ι x | φ ∈ V
4 eqsbc1 ⊢ ι x | φ ∈ V → [˙ ι x | φ / z]˙ z = y ↔ ι x | φ = y
5 3 4 syl ⊢ ∃! x φ → [˙ ι x | φ / z]˙ z = y ↔ ι x | φ = y
6 2 5 bitr3d ⊢ ∃! x φ → ∃ z ∀ x φ ↔ x = z ∧ z = y ↔ ι x | φ = y
7 equequ2 ⊢ z = y → x = z ↔ x = y
8 7 bibi2d ⊢ z = y → φ ↔ x = z ↔ φ ↔ x = y
9 8 albidv ⊢ z = y → ∀ x φ ↔ x = z ↔ ∀ x φ ↔ x = y
10 9 biimpac ⊢ ∀ x φ ↔ x = z ∧ z = y → ∀ x φ ↔ x = y
11 10 exlimiv ⊢ ∃ z ∀ x φ ↔ x = z ∧ z = y → ∀ x φ ↔ x = y
12 6 11 biimtrrdi ⊢ ∃! x φ → ι x | φ = y → ∀ x φ ↔ x = y
13 1 12 impbid2 ⊢ ∃! x φ → ∀ x φ ↔ x = y ↔ ι x | φ = y