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	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ⟨ 𝐴 , 𝐵 ⟩ 2^nd 𝐶 ↔ 𝐶 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		op2ndg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐵 )
2	1	eqeq1d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐶 ↔ 𝐵 = 𝐶 ) )
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	⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
7		fnbrfvb	⊢ ( ( 2^nd Fn V ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ V ) → ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐶 ↔ ⟨ 𝐴 , 𝐵 ⟩ 2^nd 𝐶 ) )
8	5 6 7	mp2an	⊢ ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐶 ↔ ⟨ 𝐴 , 𝐵 ⟩ 2^nd 𝐶 )
9		eqcom	⊢ ( 𝐵 = 𝐶 ↔ 𝐶 = 𝐵 )
10	2 8 9	3bitr3g	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ⟨ 𝐴 , 𝐵 ⟩ 2^nd 𝐶 ↔ 𝐶 = 𝐵 ) )