Metamath Proof Explorer


Theorem iotaexOLD

Description: Obsolete version of iotaex as of 23-Dec-2024. (Contributed by Andrew Salmon, 11-Jul-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion iotaexOLD ι x | φ V

Proof

Step Hyp Ref Expression
1 iotaval x φ x = z ι x | φ = z
2 1 eqcomd x φ x = z z = ι x | φ
3 2 eximi z x φ x = z z z = ι x | φ
4 eu6 ∃! x φ z x φ x = z
5 isset ι x | φ V z z = ι x | φ
6 3 4 5 3imtr4i ∃! x φ ι x | φ V
7 iotanul ¬ ∃! x φ ι x | φ =
8 0ex V
9 7 8 eqeltrdi ¬ ∃! x φ ι x | φ V
10 6 9 pm2.61i ι x | φ V