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

Metamath Proof Explorer

Theorem br2ndeqg

Description: Uniqueness condition for the binary relation 2nd . (Contributed by Scott Fenton, 2-Jul-2020) Revised to remove sethood hypothesis on C . (Revised by Peter Mazsa, 17-Jan-2022)

Ref Expression
Assertion br2ndeqg ⊢ A ∈ V ∧ B ∈ W → A B 2 nd C ↔ C = B

Proof

Step Hyp Ref Expression
1 op2ndg ⊢ A ∈ V ∧ B ∈ W → 2 nd ⁡ A B = B
2 1 eqeq1d ⊢ A ∈ V ∧ B ∈ W → 2 nd ⁡ A B = C ↔ B = C
3 fo2nd ⊢ 2 nd : V ⟶ onto V
4 fofn ⊢ 2 nd : V ⟶ onto V → 2 nd Fn V
5 3 4 ax-mp ⊢ 2 nd Fn V
6 opex ⊢ A B ∈ V
7 fnbrfvb ⊢ 2 nd Fn V ∧ A B ∈ V → 2 nd ⁡ A B = C ↔ A B 2 nd C
8 5 6 7 mp2an ⊢ 2 nd ⁡ A B = C ↔ A B 2 nd C
9 eqcom ⊢ B = C ↔ C = B
10 2 8 9 3bitr3g ⊢ A ∈ V ∧ B ∈ W → A B 2 nd C ↔ C = B