Theorem br1steqg

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

	Ref	Expression
Assertion	br1steqg	$$⊢\left(A\in V\wedge B\in W\right)\to \left(⟨A,B⟩1^{st}C\leftrightarrow C=A\right)$$

Proof

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