Theorem predbrg

Description: Closed form of elpredim . (Contributed by Scott Fenton, 13-Apr-2011) (Revised by NM, 5-Apr-2016)

	Ref	Expression
Assertion	predbrg	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) → 𝑌 𝑅 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		predeq3	⊢ ( 𝑥 = 𝑋 → Pred ( 𝑅 , 𝐴 , 𝑥 ) = Pred ( 𝑅 , 𝐴 , 𝑋 ) )
2	1	eleq2d	⊢ ( 𝑥 = 𝑋 → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑥 ) ↔ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) )
3		breq2	⊢ ( 𝑥 = 𝑋 → ( 𝑌 𝑅 𝑥 ↔ 𝑌 𝑅 𝑋 ) )
4	2 3	imbi12d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑥 ) → 𝑌 𝑅 𝑥 ) ↔ ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) → 𝑌 𝑅 𝑋 ) ) )
5		vex	⊢ 𝑥 ∈ V
6	5	elpredim	⊢ ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑥 ) → 𝑌 𝑅 𝑥 )
7	4 6	vtoclg	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) → 𝑌 𝑅 𝑋 ) )
8	7	imp	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) → 𝑌 𝑅 𝑋 )