Theorem iotanul2

Description: Version of iotanul using df-iota instead of dfiota2 . (Contributed by SN, 6-Nov-2024)

	Ref	Expression
Assertion	iotanul2	⊢ ( ¬ ∃ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } → ( ℩ 𝑥 𝜑 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		df-iota	⊢ ( ℩ 𝑥 𝜑 ) = ∪ { 𝑤 ∣ { 𝑥 ∣ 𝜑 } = { 𝑤 } }
2		n0	⊢ ( ∪ { 𝑤 ∣ { 𝑥 ∣ 𝜑 } = { 𝑤 } } ≠ ∅ ↔ ∃ 𝑣 𝑣 ∈ ∪ { 𝑤 ∣ { 𝑥 ∣ 𝜑 } = { 𝑤 } } )
3		eluni	⊢ ( 𝑣 ∈ ∪ { 𝑤 ∣ { 𝑥 ∣ 𝜑 } = { 𝑤 } } ↔ ∃ 𝑦 ( 𝑣 ∈ 𝑦 ∧ 𝑦 ∈ { 𝑤 ∣ { 𝑥 ∣ 𝜑 } = { 𝑤 } } ) )
4		vex	⊢ 𝑦 ∈ V
5		sneq	⊢ ( 𝑤 = 𝑦 → { 𝑤 } = { 𝑦 } )
6	5	eqeq2d	⊢ ( 𝑤 = 𝑦 → ( { 𝑥 ∣ 𝜑 } = { 𝑤 } ↔ { 𝑥 ∣ 𝜑 } = { 𝑦 } ) )
7	4 6	elab	⊢ ( 𝑦 ∈ { 𝑤 ∣ { 𝑥 ∣ 𝜑 } = { 𝑤 } } ↔ { 𝑥 ∣ 𝜑 } = { 𝑦 } )
8	7	biimpi	⊢ ( 𝑦 ∈ { 𝑤 ∣ { 𝑥 ∣ 𝜑 } = { 𝑤 } } → { 𝑥 ∣ 𝜑 } = { 𝑦 } )
9	8	adantl	⊢ ( ( 𝑣 ∈ 𝑦 ∧ 𝑦 ∈ { 𝑤 ∣ { 𝑥 ∣ 𝜑 } = { 𝑤 } } ) → { 𝑥 ∣ 𝜑 } = { 𝑦 } )
10	9	eximi	⊢ ( ∃ 𝑦 ( 𝑣 ∈ 𝑦 ∧ 𝑦 ∈ { 𝑤 ∣ { 𝑥 ∣ 𝜑 } = { 𝑤 } } ) → ∃ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } )
11	3 10	sylbi	⊢ ( 𝑣 ∈ ∪ { 𝑤 ∣ { 𝑥 ∣ 𝜑 } = { 𝑤 } } → ∃ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } )
12	11	exlimiv	⊢ ( ∃ 𝑣 𝑣 ∈ ∪ { 𝑤 ∣ { 𝑥 ∣ 𝜑 } = { 𝑤 } } → ∃ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } )
13	2 12	sylbi	⊢ ( ∪ { 𝑤 ∣ { 𝑥 ∣ 𝜑 } = { 𝑤 } } ≠ ∅ → ∃ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } )
14	13	necon1bi	⊢ ( ¬ ∃ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } → ∪ { 𝑤 ∣ { 𝑥 ∣ 𝜑 } = { 𝑤 } } = ∅ )
15	1 14	eqtrid	⊢ ( ¬ ∃ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } → ( ℩ 𝑥 𝜑 ) = ∅ )