Theorem fv1prop

Description: The function value of unordered pair of ordered pairs with first components 1 and 2 at 1. (Contributed by AV, 4-Feb-2023)

	Ref	Expression
Assertion	fv1prop	$$⊢A\in V\to \left\{⟨1,A⟩,⟨2,B⟩\right\}\left(1\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		1ex	$$⊢1\in \mathrm{V}$$
2		1ne2	$$⊢1\ne 2$$
3		fvpr1g	$$⊢\left(1\in \mathrm{V}\wedge A\in V\wedge 1\ne 2\right)\to \left\{⟨1,A⟩,⟨2,B⟩\right\}\left(1\right)=A$$
4	1 2 3	mp3an13	$$⊢A\in V\to \left\{⟨1,A⟩,⟨2,B⟩\right\}\left(1\right)=A$$