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 AVBWAB=AB

Proof

Step Hyp Ref Expression
1 vex xV
2 1 elint xAByyABxy
3 vex yV
4 3 elpr yABy=Ay=B
5 4 imbi1i yABxyy=Ay=Bxy
6 jaob y=Ay=Bxyy=Axyy=Bxy
7 5 6 bitri yABxyy=Axyy=Bxy
8 7 albii yyABxyyy=Axyy=Bxy
9 19.26 yy=Axyy=Bxyyy=Axyyy=Bxy
10 2 8 9 3bitri xAByy=Axyyy=Bxy
11 elin xABxAxB
12 clel4g AVxAyy=Axy
13 clel4g BWxByy=Bxy
14 12 13 bi2anan9 AVBWxAxByy=Axyyy=Bxy
15 11 14 bitr2id AVBWyy=Axyyy=BxyxAB
16 10 15 bitrid AVBWxABxAB
17 16 alrimiv AVBWxxABxAB
18 dfcleq AB=ABxxABxAB
19 17 18 sylibr AVBWAB=AB