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 { 𝑔𝑔 RegGraph 0 } ∉ V

Proof

Step Hyp Ref Expression
1 rusgrrgr ( 𝑔 RegUSGraph 0 → 𝑔 RegGraph 0 )
2 1 ss2abi { 𝑔𝑔 RegUSGraph 0 } ⊆ { 𝑔𝑔 RegGraph 0 }
3 rusgrprc { 𝑔𝑔 RegUSGraph 0 } ∉ V
4 prcssprc ( ( { 𝑔𝑔 RegUSGraph 0 } ⊆ { 𝑔𝑔 RegGraph 0 } ∧ { 𝑔𝑔 RegUSGraph 0 } ∉ V ) → { 𝑔𝑔 RegGraph 0 } ∉ V )
5 2 3 4 mp2an { 𝑔𝑔 RegGraph 0 } ∉ V