Theorem bj-nuliotaALT

Description: Alternate proof of bj-nuliota . Note that this alternate proof uses the fact that iota x ph evaluates to (/) when there is no x satisfying ph ( iotanul ). This is an implementation detail of the encoding currently used in set.mm and should be avoided. (Contributed by BJ, 30-Nov-2019) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	bj-nuliotaALT	⊢ ∅ = ( ℩ 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		0ss	⊢ ∅ ⊆ ( ℩ 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 )
2		iotassuni	⊢ ( ℩ 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 ) ⊆ ∪ { 𝑥 ∣ ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 }
3		eq0	⊢ ( 𝑥 = ∅ ↔ ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 )
4	3	bicomi	⊢ ( ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 ↔ 𝑥 = ∅ )
5	4	abbii	⊢ { 𝑥 ∣ ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 } = { 𝑥 ∣ 𝑥 = ∅ }
6	5	unieqi	⊢ ∪ { 𝑥 ∣ ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 } = ∪ { 𝑥 ∣ 𝑥 = ∅ }
7		df-sn	⊢ { ∅ } = { 𝑥 ∣ 𝑥 = ∅ }
8	7	eqcomi	⊢ { 𝑥 ∣ 𝑥 = ∅ } = { ∅ }
9	8	unieqi	⊢ ∪ { 𝑥 ∣ 𝑥 = ∅ } = ∪ { ∅ }
10		0ex	⊢ ∅ ∈ V
11	10	unisn	⊢ ∪ { ∅ } = ∅
12	6 9 11	3eqtri	⊢ ∪ { 𝑥 ∣ ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 } = ∅
13	2 12	sseqtri	⊢ ( ℩ 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 ) ⊆ ∅
14	1 13	eqssi	⊢ ∅ = ( ℩ 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 )