Metamath Proof Explorer


Theorem iotauni2

Description: Version of iotauni using df-iota instead of dfiota2 . (Contributed by SN, 6-Nov-2024)

Ref Expression
Assertion iotauni2 y x | φ = y ι x | φ = x | φ

Proof

Step Hyp Ref Expression
1 iotaval2 x | φ = y ι x | φ = y
2 unieq x | φ = y x | φ = y
3 unisnv y = y
4 2 3 eqtr2di x | φ = y y = x | φ
5 1 4 eqtrd x | φ = y ι x | φ = x | φ
6 5 exlimiv y x | φ = y ι x | φ = x | φ