Theorem fv2prop

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	fv2prop	$$⊢B\in V\to \left\{⟨1,A⟩,⟨2,B⟩\right\}\left(2\right)=B$$

Proof

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