Metamath Proof Explorer

Theorem br2ndeq

Description: Uniqueness condition for the binary relation 2nd . (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 br2ndeq ⊢ A B 2 nd C ↔ C = B

Proof

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