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 e. _V |
|
| intpr.2 | |- B e. _V |
||
| Assertion | intpr | |- |^| { A , B } = ( A i^i B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | intpr.1 | |- A e. _V |
|
| 2 | intpr.2 | |- B e. _V |
|
| 3 | intprg | |- ( ( A e. _V /\ B e. _V ) -> |^| { A , B } = ( A i^i B ) ) |
|
| 4 | 1 2 3 | mp2an | |- |^| { A , B } = ( A i^i B ) |