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 abbi1 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 | ψ