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

Metamath Proof Explorer

Theorem iotauni

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

Ref Expression
Assertion iotauni ⊢ ∃! x φ → ι x | φ = ⋃ x | φ

Proof

Step Hyp Ref Expression
1 eu6 ⊢ ∃! x φ ↔ ∃ z ∀ x φ ↔ x = z
2 iotaval ⊢ ∀ x φ ↔ x = z → ι x | φ = z
3 uniabio ⊢ ∀ x φ ↔ x = z → ⋃ x | φ = z
4 2 3 eqtr4d ⊢ ∀ x φ ↔ x = z → ι x | φ = ⋃ x | φ
5 4 exlimiv ⊢ ∃ z ∀ x φ ↔ x = z → ι x | φ = ⋃ x | φ
6 1 5 sylbi ⊢ ∃! x φ → ι x | φ = ⋃ x | φ