Theorem 0iin

Description: An empty indexed intersection is the universal class. (Contributed by NM, 20-Oct-2005)

	Ref	Expression
Assertion	0iin	⊢ ∩ 𝑥 ∈ ∅ 𝐴 = V

Proof

Step	Hyp	Ref	Expression
1		df-iin	⊢ ∩ 𝑥 ∈ ∅ 𝐴 = { 𝑦 ∣ ∀ 𝑥 ∈ ∅ 𝑦 ∈ 𝐴 }
2		vex	⊢ 𝑦 ∈ V
3		ral0	⊢ ∀ 𝑥 ∈ ∅ 𝑦 ∈ 𝐴
4	2 3	2th	⊢ ( 𝑦 ∈ V ↔ ∀ 𝑥 ∈ ∅ 𝑦 ∈ 𝐴 )
5	4	abbi2i	⊢ V = { 𝑦 ∣ ∀ 𝑥 ∈ ∅ 𝑦 ∈ 𝐴 }
6	1 5	eqtr4i	⊢ ∩ 𝑥 ∈ ∅ 𝐴 = V