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 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 intprg A V B V A B = A B
4 1 2 3 mp2an A B = A B