Theorem dfpred2

Description: An alternate definition of predecessor class when X is a set. (Contributed by Scott Fenton, 8-Feb-2011)

	Ref	Expression
Hypothesis	dfpred2.1	⊢ 𝑋 ∈ V
Assertion	dfpred2	⊢ Pred ( 𝑅 , 𝐴 , 𝑋 ) = ( 𝐴 ∩ { 𝑦 ∣ 𝑦 𝑅 𝑋 } )

Proof

Step	Hyp	Ref	Expression
1		dfpred2.1	⊢ 𝑋 ∈ V
2		df-pred	⊢ Pred ( 𝑅 , 𝐴 , 𝑋 ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) )
3		iniseg	⊢ ( 𝑋 ∈ V → ( ◡ 𝑅 “ { 𝑋 } ) = { 𝑦 ∣ 𝑦 𝑅 𝑋 } )
4	1 3	ax-mp	⊢ ( ◡ 𝑅 “ { 𝑋 } ) = { 𝑦 ∣ 𝑦 𝑅 𝑋 }
5	4	ineq2i	⊢ ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) = ( 𝐴 ∩ { 𝑦 ∣ 𝑦 𝑅 𝑋 } )
6	2 5	eqtri	⊢ Pred ( 𝑅 , 𝐴 , 𝑋 ) = ( 𝐴 ∩ { 𝑦 ∣ 𝑦 𝑅 𝑋 } )