Theorem pred0

Description: The predecessor class over (/) is always (/) . (Contributed by Scott Fenton, 16-Apr-2011) (Proof shortened by AV, 11-Jun-2021)

	Ref	Expression
Assertion	pred0	⊢ Pred ( 𝑅 , ∅ , 𝑋 ) = ∅

Proof

Step	Hyp	Ref	Expression
1		df-pred	⊢ Pred ( 𝑅 , ∅ , 𝑋 ) = ( ∅ ∩ ( ◡ 𝑅 “ { 𝑋 } ) )
2		0in	⊢ ( ∅ ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) = ∅
3	1 2	eqtri	⊢ Pred ( 𝑅 , ∅ , 𝑋 ) = ∅