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

Proof

Step	Hyp	Ref	Expression
1		op1stg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐴 )
2	1	eqeq1d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐶 ↔ 𝐴 = 𝐶 ) )
3		fo1st	⊢ 1st : V –onto→ V
4		fofn	⊢ ( 1st : V –onto→ V → 1st Fn V )
5	3 4	ax-mp	⊢ 1st Fn V
6		opex	⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
7		fnbrfvb	⊢ ( ( 1st Fn V ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ V ) → ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐶 ↔ ⟨ 𝐴 , 𝐵 ⟩ 1st 𝐶 ) )
8	5 6 7	mp2an	⊢ ( ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐶 ↔ ⟨ 𝐴 , 𝐵 ⟩ 1st 𝐶 )
9		eqcom	⊢ ( 𝐴 = 𝐶 ↔ 𝐶 = 𝐴 )
10	2 8 9	3bitr3g	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ⟨ 𝐴 , 𝐵 ⟩ 1st 𝐶 ↔ 𝐶 = 𝐴 ) )