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 ( ℩ 𝑥 𝜑 ) ∈ 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