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) Prove from intprg . (Revised by BJ, 1-Sep-2024)

Ref Expression
Hypotheses intpr.1 AV
intpr.2 BV
Assertion intpr AB=AB

Proof

Step Hyp Ref Expression
1 intpr.1 AV
2 intpr.2 BV
3 intprg AVBVAB=AB
4 1 2 3 mp2an AB=AB