Theorem inteq

Description: Equality law for intersection. (Contributed by NM, 13-Sep-1999)

	Ref	Expression
Assertion	inteq	⊢ ( 𝐴 = 𝐵 → ∩ 𝐴 = ∩ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		raleq	⊢ ( 𝐴 = 𝐵 → ( ∀ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ↔ ∀ 𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 ) )
2	1	abbidv	⊢ ( 𝐴 = 𝐵 → { 𝑥 ∣ ∀ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 } = { 𝑥 ∣ ∀ 𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 } )
3		dfint2	⊢ ∩ 𝐴 = { 𝑥 ∣ ∀ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 }
4		dfint2	⊢ ∩ 𝐵 = { 𝑥 ∣ ∀ 𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 }
5	2 3 4	3eqtr4g	⊢ ( 𝐴 = 𝐵 → ∩ 𝐴 = ∩ 𝐵 )