Theorem dfpred3

Description: An alternate definition of predecessor class when X is a set. (Contributed by Scott Fenton, 13-Jun-2018)

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

Proof

Step	Hyp	Ref	Expression
1		dfpred2.1	⊢ 𝑋 ∈ V
2		incom	⊢ ( 𝐴 ∩ { 𝑦 ∣ 𝑦 𝑅 𝑋 } ) = ( { 𝑦 ∣ 𝑦 𝑅 𝑋 } ∩ 𝐴 )
3	1	dfpred2	⊢ Pred ( 𝑅 , 𝐴 , 𝑋 ) = ( 𝐴 ∩ { 𝑦 ∣ 𝑦 𝑅 𝑋 } )
4		dfrab2	⊢ { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑋 } = ( { 𝑦 ∣ 𝑦 𝑅 𝑋 } ∩ 𝐴 )
5	2 3 4	3eqtr4i	⊢ Pred ( 𝑅 , 𝐴 , 𝑋 ) = { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑋 }