# Metamath Proof Explorer

## 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
`|- ( ( A e. V /\ B e. W ) -> |^| { A , B } = ( A i^i B ) )`

### Proof

Step Hyp Ref Expression
1 preq1
` |-  ( x = A -> { x , y } = { A , y } )`
2 1 inteqd
` |-  ( x = A -> |^| { x , y } = |^| { A , y } )`
3 ineq1
` |-  ( x = A -> ( x i^i y ) = ( A i^i y ) )`
4 2 3 eqeq12d
` |-  ( x = A -> ( |^| { x , y } = ( x i^i y ) <-> |^| { A , y } = ( A i^i y ) ) )`
5 preq2
` |-  ( y = B -> { A , y } = { A , B } )`
6 5 inteqd
` |-  ( y = B -> |^| { A , y } = |^| { A , B } )`
7 ineq2
` |-  ( y = B -> ( A i^i y ) = ( A i^i B ) )`
8 6 7 eqeq12d
` |-  ( y = B -> ( |^| { A , y } = ( A i^i y ) <-> |^| { A , B } = ( A i^i B ) ) )`
9 vex
` |-  x e. _V`
10 vex
` |-  y e. _V`
11 9 10 intpr
` |-  |^| { x , y } = ( x i^i y )`
12 4 8 11 vtocl2g
` |-  ( ( A e. V /\ B e. W ) -> |^| { A , B } = ( A i^i B ) )`