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	⊢ 𝑈 = { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 : ∅ ⟶ ∅ }
Assertion	griedg0prc	⊢ 𝑈 ∉ V

Proof

Step	Hyp	Ref	Expression
1		griedg0prc.u	⊢ 𝑈 = { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 : ∅ ⟶ ∅ }
2		0ex	⊢ ∅ ∈ V
3		feq1	⊢ ( 𝑒 = ∅ → ( 𝑒 : ∅ ⟶ ∅ ↔ ∅ : ∅ ⟶ ∅ ) )
4		f0	⊢ ∅ : ∅ ⟶ ∅
5	2 3 4	ceqsexv2d	⊢ ∃ 𝑒 𝑒 : ∅ ⟶ ∅
6		opabn1stprc	⊢ ( ∃ 𝑒 𝑒 : ∅ ⟶ ∅ → { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 : ∅ ⟶ ∅ } ∉ V )
7	5 6	ax-mp	⊢ { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 : ∅ ⟶ ∅ } ∉ V
8		neleq1	⊢ ( 𝑈 = { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 : ∅ ⟶ ∅ } → ( 𝑈 ∉ V ↔ { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 : ∅ ⟶ ∅ } ∉ V ) )
9	1 8	ax-mp	⊢ ( 𝑈 ∉ V ↔ { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 : ∅ ⟶ ∅ } ∉ V )
10	7 9	mpbir	⊢ 𝑈 ∉ V