Theorem dfpred3g

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

	Ref	Expression
Assertion	dfpred3g	⊢ ( 𝑋 ∈ 𝑉 → Pred ( 𝑅 , 𝐴 , 𝑋 ) = { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑋 } )

Proof

Step	Hyp	Ref	Expression
1		predeq3	⊢ ( 𝑥 = 𝑋 → Pred ( 𝑅 , 𝐴 , 𝑥 ) = Pred ( 𝑅 , 𝐴 , 𝑋 ) )
2		breq2	⊢ ( 𝑥 = 𝑋 → ( 𝑦 𝑅 𝑥 ↔ 𝑦 𝑅 𝑋 ) )
3	2	rabbidv	⊢ ( 𝑥 = 𝑋 → { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } = { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑋 } )
4	1 3	eqeq12d	⊢ ( 𝑥 = 𝑋 → ( Pred ( 𝑅 , 𝐴 , 𝑥 ) = { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } ↔ Pred ( 𝑅 , 𝐴 , 𝑋 ) = { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑋 } ) )
5		vex	⊢ 𝑥 ∈ V
6	5	dfpred3	⊢ Pred ( 𝑅 , 𝐴 , 𝑥 ) = { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 }
7	4 6	vtoclg	⊢ ( 𝑋 ∈ 𝑉 → Pred ( 𝑅 , 𝐴 , 𝑋 ) = { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑋 } )