Metamath Proof Explorer


Theorem intpr

Description: The intersection of a pair is the intersection of its members. Theorem 71 of Suppes p. 42. (Contributed by NM, 14-Oct-1999)

Ref Expression
Hypotheses intpr.1 A V
intpr.2 B V
Assertion intpr A B = A B

Proof

Step Hyp Ref Expression
1 intpr.1 A V
2 intpr.2 B V
3 19.26 y y = A x y y = B x y y y = A x y y y = B x y
4 vex y V
5 4 elpr y A B y = A y = B
6 5 imbi1i y A B x y y = A y = B x y
7 jaob y = A y = B x y y = A x y y = B x y
8 6 7 bitri y A B x y y = A x y y = B x y
9 8 albii y y A B x y y y = A x y y = B x y
10 1 clel4 x A y y = A x y
11 2 clel4 x B y y = B x y
12 10 11 anbi12i x A x B y y = A x y y y = B x y
13 3 9 12 3bitr4i y y A B x y x A x B
14 vex x V
15 14 elint x A B y y A B x y
16 elin x A B x A x B
17 13 15 16 3bitr4i x A B x A B
18 17 eqriv A B = A B