Definition df-gric

Description: Two graphs are said to be isomorphic iff they are connected by at least one isomorphism, see definition in Diestel p. 3 and definition in Bollobas p. 3. Isomorphic graphs share all global graph properties like order and size. (Contributed by AV, 11-Nov-2022) (Revised by AV, 19-Apr-2025)

	Ref	Expression
Assertion	df-gric	|- ~=gr = ( `' GraphIso " ( _V \ 1o ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgric	|- ~=gr
1		cgrim	|- GraphIso
2	1	ccnv	|- `' GraphIso
3		cvv	|- _V
4		c1o	|- 1o
5	3 4	cdif	|- ( _V \ 1o )
6	2 5	cima	|- ( `' GraphIso " ( _V \ 1o ) )
7	0 6	wceq	|- ~=gr = ( `' GraphIso " ( _V \ 1o ) )