Theorem gropd

Description: If any representation of a graph with vertices V and edges E has a certain property ps , then the ordered pair <. V , E >. of the set of vertices and the set of edges (which is such a representation of a graph with vertices V and edges E ) has this property. (Contributed by AV, 11-Oct-2020)

	Ref	Expression
Hypotheses	gropd.g	⊢ ( 𝜑 → ∀ 𝑔 ( ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = 𝐸 ) → 𝜓 ) )
	gropd.v	⊢ ( 𝜑 → 𝑉 ∈ 𝑈 )
	gropd.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑊 )
Assertion	gropd	⊢ ( 𝜑 → [ ⟨ 𝑉 , 𝐸 ⟩ / 𝑔 ] 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		gropd.g	⊢ ( 𝜑 → ∀ 𝑔 ( ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = 𝐸 ) → 𝜓 ) )
2		gropd.v	⊢ ( 𝜑 → 𝑉 ∈ 𝑈 )
3		gropd.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑊 )
4		opex	⊢ ⟨ 𝑉 , 𝐸 ⟩ ∈ V
5	4	a1i	⊢ ( 𝜑 → ⟨ 𝑉 , 𝐸 ⟩ ∈ V )
6		opvtxfv	⊢ ( ( 𝑉 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) → ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉 )
7		opiedgfv	⊢ ( ( 𝑉 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) → ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸 )
8	6 7	jca	⊢ ( ( 𝑉 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) → ( ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉 ∧ ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸 ) )
9	2 3 8	syl2anc	⊢ ( 𝜑 → ( ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉 ∧ ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸 ) )
10		nfcv	⊢ Ⅎ 𝑔 ⟨ 𝑉 , 𝐸 ⟩
11		nfv	⊢ Ⅎ 𝑔 ( ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉 ∧ ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸 )
12		nfsbc1v	⊢ Ⅎ 𝑔 [ ⟨ 𝑉 , 𝐸 ⟩ / 𝑔 ] 𝜓
13	11 12	nfim	⊢ Ⅎ 𝑔 ( ( ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉 ∧ ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸 ) → [ ⟨ 𝑉 , 𝐸 ⟩ / 𝑔 ] 𝜓 )
14		fveqeq2	⊢ ( 𝑔 = ⟨ 𝑉 , 𝐸 ⟩ → ( ( Vtx ‘ 𝑔 ) = 𝑉 ↔ ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉 ) )
15		fveqeq2	⊢ ( 𝑔 = ⟨ 𝑉 , 𝐸 ⟩ → ( ( iEdg ‘ 𝑔 ) = 𝐸 ↔ ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸 ) )
16	14 15	anbi12d	⊢ ( 𝑔 = ⟨ 𝑉 , 𝐸 ⟩ → ( ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = 𝐸 ) ↔ ( ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉 ∧ ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸 ) ) )
17		sbceq1a	⊢ ( 𝑔 = ⟨ 𝑉 , 𝐸 ⟩ → ( 𝜓 ↔ [ ⟨ 𝑉 , 𝐸 ⟩ / 𝑔 ] 𝜓 ) )
18	16 17	imbi12d	⊢ ( 𝑔 = ⟨ 𝑉 , 𝐸 ⟩ → ( ( ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = 𝐸 ) → 𝜓 ) ↔ ( ( ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉 ∧ ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸 ) → [ ⟨ 𝑉 , 𝐸 ⟩ / 𝑔 ] 𝜓 ) ) )
19	10 13 18	spcgf	⊢ ( ⟨ 𝑉 , 𝐸 ⟩ ∈ V → ( ∀ 𝑔 ( ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = 𝐸 ) → 𝜓 ) → ( ( ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉 ∧ ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸 ) → [ ⟨ 𝑉 , 𝐸 ⟩ / 𝑔 ] 𝜓 ) ) )
20	5 1 9 19	syl3c	⊢ ( 𝜑 → [ ⟨ 𝑉 , 𝐸 ⟩ / 𝑔 ] 𝜓 )