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)

	Ref	Expression
Assertion	iotaex	⊢ ( ℩ 𝑥 𝜑 ) ∈ V

Proof

Step	Hyp	Ref	Expression
1		iotaval	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) → ( ℩ 𝑥 𝜑 ) = 𝑧 )
2	1	eqcomd	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) → 𝑧 = ( ℩ 𝑥 𝜑 ) )
3	2	eximi	⊢ ( ∃ 𝑧 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) → ∃ 𝑧 𝑧 = ( ℩ 𝑥 𝜑 ) )
4		eu6	⊢ ( ∃! 𝑥 𝜑 ↔ ∃ 𝑧 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) )
5		isset	⊢ ( ( ℩ 𝑥 𝜑 ) ∈ V ↔ ∃ 𝑧 𝑧 = ( ℩ 𝑥 𝜑 ) )
6	3 4 5	3imtr4i	⊢ ( ∃! 𝑥 𝜑 → ( ℩ 𝑥 𝜑 ) ∈ V )
7		iotanul	⊢ ( ¬ ∃! 𝑥 𝜑 → ( ℩ 𝑥 𝜑 ) = ∅ )
8		0ex	⊢ ∅ ∈ V
9	7 8	eqeltrdi	⊢ ( ¬ ∃! 𝑥 𝜑 → ( ℩ 𝑥 𝜑 ) ∈ V )
10	6 9	pm2.61i	⊢ ( ℩ 𝑥 𝜑 ) ∈ V