Theorem griedg0prc

Description: The class of empty graphs (represented as ordered pairs) is a proper class. (Contributed by AV, 27-Dec-2020)

	Ref	Expression
Hypothesis	griedg0prc.u	|- U = { <. v , e >. | e : (/) --> (/) }
Assertion	griedg0prc	|- U e/ _V

Proof

Step	Hyp	Ref	Expression
1		griedg0prc.u	|- U = { <. v , e >. | e : (/) --> (/) }
2		0ex	|- (/) e. _V
3		feq1	|- ( e = (/) -> ( e : (/) --> (/) <-> (/) : (/) --> (/) ) )
4		f0	|- (/) : (/) --> (/)
5	2 3 4	ceqsexv2d	|- E. e e : (/) --> (/)
6		opabn1stprc	|- ( E. e e : (/) --> (/) -> { <. v , e >. | e : (/) --> (/) } e/ _V )
7	5 6	ax-mp	|- { <. v , e >. | e : (/) --> (/) } e/ _V
8		neleq1	|- ( U = { <. v , e >. | e : (/) --> (/) } -> ( U e/ _V <-> { <. v , e >. | e : (/) --> (/) } e/ _V ) )
9	1 8	ax-mp	|- ( U e/ _V <-> { <. v , e >. | e : (/) --> (/) } e/ _V )
10	7 9	mpbir	|- U e/ _V