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) (Proof shortened by BJ, 1-Sep-2024)

Ref Expression
Assertion intprg A V B W A B = A B

Proof

Step Hyp Ref Expression
1 vex x V
2 1 elint x A B y y A B x y
3 vex y V
4 3 elpr y A B y = A y = B
5 4 imbi1i y A B x y y = A y = B x y
6 jaob y = A y = B x y y = A x y y = B x y
7 5 6 bitri y A B x y y = A x y y = B x y
8 7 albii y y A B x y y y = A x y y = B x y
9 19.26 y y = A x y y = B x y y y = A x y y y = B x y
10 2 8 9 3bitri x A B y y = A x y y y = B x y
11 elin x A B x A x B
12 clel4g A V x A y y = A x y
13 clel4g B W x B y y = B x y
14 12 13 bi2anan9 A V B W x A x B y y = A x y y y = B x y
15 11 14 bitr2id A V B W y y = A x y y y = B x y x A B
16 10 15 syl5bb A V B W x A B x A B
17 16 alrimiv A V B W x x A B x A B
18 dfcleq A B = A B x x A B x A B
19 17 18 sylibr A V B W A B = A B