Metamath Proof Explorer


Theorem iotaex

Description: Theorem 8.23 in Quine p. 58. This theorem proves the existence of the iota class under our definition. (Contributed by Andrew Salmon, 11-Jul-2011) Remove dependency on ax-10 , ax-11 , ax-12 . (Revised by SN, 6-Nov-2024)

Ref Expression
Assertion iotaex ι x | φ V

Proof

Step Hyp Ref Expression
1 iotaval2 x | φ = y ι x | φ = y
2 vex y V
3 1 2 eqeltrdi x | φ = y ι x | φ V
4 3 exlimiv y x | φ = y ι x | φ V
5 iotanul2 ¬ y x | φ = y ι x | φ =
6 0ex V
7 5 6 eqeltrdi ¬ y x | φ = y ι x | φ V
8 4 7 pm2.61i ι x | φ V