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	$$⊢\left(A\in V\wedge B\in W\right)\to \left(⟨A,B⟩2^{nd}C\leftrightarrow C=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		op2ndg	$$⊢\left(A\in V\wedge B\in W\right)\to 2^{nd}\left(⟨A,B⟩\right)=B$$
2	1	eqeq1d	$$⊢\left(A\in V\wedge B\in W\right)\to \left(2^{nd}\left(⟨A,B⟩\right)=C\leftrightarrow B=C\right)$$
3		fo2nd	$$⊢2^{nd}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}$$
4		fofn	$$⊢2^{nd}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}\to 2^{nd}Fn\mathrm{V}$$
5	3 4	ax-mp	$$⊢2^{nd}Fn\mathrm{V}$$
6		opex	$$⊢⟨A,B⟩\in \mathrm{V}$$
7		fnbrfvb	$$⊢\left(2^{nd}Fn\mathrm{V}\wedge ⟨A,B⟩\in \mathrm{V}\right)\to \left(2^{nd}\left(⟨A,B⟩\right)=C\leftrightarrow ⟨A,B⟩2^{nd}C\right)$$
8	5 6 7	mp2an	$$⊢2^{nd}\left(⟨A,B⟩\right)=C\leftrightarrow ⟨A,B⟩2^{nd}C$$
9		eqcom	$$⊢B=C\leftrightarrow C=B$$
10	2 8 9	3bitr3g	$$⊢\left(A\in V\wedge B\in W\right)\to \left(⟨A,B⟩2^{nd}C\leftrightarrow C=B\right)$$