This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem op1stb

Description: Extract the first member of an ordered pair. Theorem 73 of Suppes p. 42. (See op2ndb to extract the second member, op1sta for an alternate version, and op1st for the preferred version.) (Contributed by NM, 25-Nov-2003)

Ref Expression
Hypotheses op1stb.1 ⊢ A ∈ V
op1stb.2 ⊢ B ∈ V
Assertion op1stb ⊢ ⋂ ⋂ A B = A

Proof

Step Hyp Ref Expression
1 op1stb.1 ⊢ A ∈ V
2 op1stb.2 ⊢ B ∈ V
3 1 2 dfop ⊢ A B = A A B
4 3 inteqi ⊢ ⋂ A B = ⋂ A A B
5 snex ⊢ A ∈ V
6 prex ⊢ A B ∈ V
7 5 6 intpr ⊢ ⋂ A A B = A ∩ A B
8 snsspr1 ⊢ A ⊆ A B
9 dfss2 ⊢ A ⊆ A B ↔ A ∩ A B = A
10 8 9 mpbi ⊢ A ∩ A B = A
11 7 10 eqtri ⊢ ⋂ A A B = A
12 4 11 eqtri ⊢ ⋂ A B = A
13 12 inteqi ⊢ ⋂ ⋂ A B = ⋂ A
14 1 intsn ⊢ ⋂ A = A
15 13 14 eqtri ⊢ ⋂ ⋂ A B = A