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

Metamath Proof Explorer

Theorem iotabi

Description: Equivalence theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011)

Ref Expression
Assertion iotabi ⊢ ∀ x φ ↔ ψ → ι x | φ = ι x | ψ

Proof

Step Hyp Ref Expression
1 abbi ⊢ ∀ x φ ↔ ψ → x | φ = x | ψ
2 1 eqeq1d ⊢ ∀ x φ ↔ ψ → x | φ = z ↔ x | ψ = z
3 2 abbidv ⊢ ∀ x φ ↔ ψ → z | x | φ = z = z | x | ψ = z
4 3 unieqd ⊢ ∀ x φ ↔ ψ → ⋃ z | x | φ = z = ⋃ z | x | ψ = z
5 df-iota ⊢ ι x | φ = ⋃ z | x | φ = z
6 df-iota ⊢ ι x | ψ = ⋃ z | x | ψ = z
7 4 5 6 3eqtr4g ⊢ ∀ x φ ↔ ψ → ι x | φ = ι x | ψ