Theorem opvtxval

Description: The set of vertices of a graph represented as an ordered pair of vertices and indexed edges. (Contributed by AV, 9-Jan-2020) (Revised by AV, 21-Sep-2020)

	Ref	Expression
Assertion	opvtxval	$$⊢G\in \left(\mathrm{V}\times \mathrm{V}\right)\to \mathrm{Vtx}\left(G\right)=1^{st}\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		vtxval	$$⊢\mathrm{Vtx}\left(G\right)=if\left(G\in \left(\mathrm{V}\times \mathrm{V}\right),1^{st}\left(G\right),{\mathrm{Base}}_G\right)$$
2		iftrue	$$⊢G\in \left(\mathrm{V}\times \mathrm{V}\right)\to if\left(G\in \left(\mathrm{V}\times \mathrm{V}\right),1^{st}\left(G\right),{\mathrm{Base}}_G\right)=1^{st}\left(G\right)$$
3	1 2	syl5eq	$$⊢G\in \left(\mathrm{V}\times \mathrm{V}\right)\to \mathrm{Vtx}\left(G\right)=1^{st}\left(G\right)$$