Theorem dfint2

Description: Alternate definition of class intersection. (Contributed by NM, 28-Jun-1998)

	Ref	Expression
Assertion	dfint2	⊢ ∩ 𝐴 = { 𝑥 ∣ ∀ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 }

Proof

Step	Hyp	Ref	Expression
1		df-int	⊢ ∩ 𝐴 = { 𝑥 ∣ ∀ 𝑦 ( 𝑦 ∈ 𝐴 → 𝑥 ∈ 𝑦 ) }
2		df-ral	⊢ ( ∀ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 → 𝑥 ∈ 𝑦 ) )
3	2	abbii	⊢ { 𝑥 ∣ ∀ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 } = { 𝑥 ∣ ∀ 𝑦 ( 𝑦 ∈ 𝐴 → 𝑥 ∈ 𝑦 ) }
4	1 3	eqtr4i	⊢ ∩ 𝐴 = { 𝑥 ∣ ∀ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 }