Theorem intprg

Description: The intersection of a pair is the intersection of its members. Closed form of intpr . Theorem 71 of Suppes p. 42. (Contributed by FL, 27-Apr-2008)

	Ref	Expression
Assertion	intprg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ∩ { 𝐴 , 𝐵 } = ( 𝐴 ∩ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		preq1	⊢ ( 𝑥 = 𝐴 → { 𝑥 , 𝑦 } = { 𝐴 , 𝑦 } )
2	1	inteqd	⊢ ( 𝑥 = 𝐴 → ∩ { 𝑥 , 𝑦 } = ∩ { 𝐴 , 𝑦 } )
3		ineq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∩ 𝑦 ) = ( 𝐴 ∩ 𝑦 ) )
4	2 3	eqeq12d	⊢ ( 𝑥 = 𝐴 → ( ∩ { 𝑥 , 𝑦 } = ( 𝑥 ∩ 𝑦 ) ↔ ∩ { 𝐴 , 𝑦 } = ( 𝐴 ∩ 𝑦 ) ) )
5		preq2	⊢ ( 𝑦 = 𝐵 → { 𝐴 , 𝑦 } = { 𝐴 , 𝐵 } )
6	5	inteqd	⊢ ( 𝑦 = 𝐵 → ∩ { 𝐴 , 𝑦 } = ∩ { 𝐴 , 𝐵 } )
7		ineq2	⊢ ( 𝑦 = 𝐵 → ( 𝐴 ∩ 𝑦 ) = ( 𝐴 ∩ 𝐵 ) )
8	6 7	eqeq12d	⊢ ( 𝑦 = 𝐵 → ( ∩ { 𝐴 , 𝑦 } = ( 𝐴 ∩ 𝑦 ) ↔ ∩ { 𝐴 , 𝐵 } = ( 𝐴 ∩ 𝐵 ) ) )
9		vex	⊢ 𝑥 ∈ V
10		vex	⊢ 𝑦 ∈ V
11	9 10	intpr	⊢ ∩ { 𝑥 , 𝑦 } = ( 𝑥 ∩ 𝑦 )
12	4 8 11	vtocl2g	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ∩ { 𝐴 , 𝐵 } = ( 𝐴 ∩ 𝐵 ) )