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

Metamath Proof Explorer

Theorem iotain

Description: Equivalence between two different forms of iota . (Contributed by Andrew Salmon, 15-Jul-2011)

Ref Expression
Assertion iotain ⊢ ∃! x φ → ⋂ x | φ = ι x | φ

Proof

Step Hyp Ref Expression
1 eu6 ⊢ ∃! x φ ↔ ∃ y ∀ x φ ↔ x = y
2 vex ⊢ y ∈ V
3 2 intsn ⊢ ⋂ y = y
4 abbi ⊢ ∀ x φ ↔ x = y → x | φ = x | x = y
5 df-sn ⊢ y = x | x = y
6 4 5 eqtr4di ⊢ ∀ x φ ↔ x = y → x | φ = y
7 6 inteqd ⊢ ∀ x φ ↔ x = y → ⋂ x | φ = ⋂ y
8 iotaval ⊢ ∀ x φ ↔ x = y → ι x | φ = y
9 3 7 8 3eqtr4a ⊢ ∀ x φ ↔ x = y → ⋂ x | φ = ι x | φ
10 9 exlimiv ⊢ ∃ y ∀ x φ ↔ x = y → ⋂ x | φ = ι x | φ
11 1 10 sylbi ⊢ ∃! x φ → ⋂ x | φ = ι x | φ