This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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