Metamath Proof Explorer

Theorem rgrprc

Description: The class of 0-regular graphs is a proper class. (Contributed by AV, 27-Dec-2020)

Ref Expression
Assertion rgrprc 
|- { g | g RegGraph 0 } e/ _V

Proof

Step Hyp Ref Expression
1 rusgrrgr 
 |-  ( g RegUSGraph 0 -> g RegGraph 0 )
2 1 ss2abi 
 |-  { g | g RegUSGraph 0 } C_ { g | g RegGraph 0 }
3 rusgrprc 
 |-  { g | g RegUSGraph 0 } e/ _V
4 prcssprc 
 |-  ( ( { g | g RegUSGraph 0 } C_ { g | g RegGraph 0 } /\ { g | g RegUSGraph 0 } e/ _V ) -> { g | g RegGraph 0 } e/ _V )
5 2 3 4 mp2an 
 |-  { g | g RegGraph 0 } e/ _V