Metamath Proof Explorer

Theorem br1steq

Description: Uniqueness condition for the binary relation 1st . (Contributed by Scott Fenton, 11-Apr-2014) (Proof shortened by Mario Carneiro, 3-May-2015)

Ref Expression
Hypotheses br1steq.1 ⊢ A ∈ V
br1steq.2 ⊢ B ∈ V
Assertion br1steq ⊢ A B 1 st C ↔ C = A

Proof

Step Hyp Ref Expression
1 br1steq.1 ⊢ A ∈ V
2 br1steq.2 ⊢ B ∈ V
3 br1steqg ⊢ A ∈ V ∧ B ∈ V → A B 1 st C ↔ C = A
4 1 2 3 mp2an ⊢ A B 1 st C ↔ C = A