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

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