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

Metamath Proof Explorer

Theorem opeldm

Description: Membership of first of an ordered pair in a domain. (Contributed by NM, 30-Jul-1995)

Ref Expression
Hypotheses opeldm.1 ⊢ A ∈ V
opeldm.2 ⊢ B ∈ V
Assertion opeldm ⊢ A B ∈ C → A ∈ dom ⁡ C

Proof

Step Hyp Ref Expression
1 opeldm.1 ⊢ A ∈ V
2 opeldm.2 ⊢ B ∈ V
3 opeq2 ⊢ y = B → A y = A B
4 3 eleq1d ⊢ y = B → A y ∈ C ↔ A B ∈ C
5 2 4 spcev ⊢ A B ∈ C → ∃ y A y ∈ C
6 1 eldm2 ⊢ A ∈ dom ⁡ C ↔ ∃ y A y ∈ C
7 5 6 sylibr ⊢ A B ∈ C → A ∈ dom ⁡ C