Theorem predep

Description: The predecessor under the membership relation is equivalent to an intersection. (Contributed by Scott Fenton, 27-Mar-2011) (Proof shortened by Andrew Salmon, 27-Aug-2011)

	Ref	Expression
Assertion	predep	⊢ ( 𝑋 ∈ 𝐵 → Pred ( E , 𝐴 , 𝑋 ) = ( 𝐴 ∩ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		df-pred	⊢ Pred ( E , 𝐴 , 𝑋 ) = ( 𝐴 ∩ ( ◡ E “ { 𝑋 } ) )
2		relcnv	⊢ Rel ◡ E
3		relimasn	⊢ ( Rel ◡ E → ( ◡ E “ { 𝑋 } ) = { 𝑦 ∣ 𝑋 ◡ E 𝑦 } )
4	2 3	ax-mp	⊢ ( ◡ E “ { 𝑋 } ) = { 𝑦 ∣ 𝑋 ◡ E 𝑦 }
5		brcnvg	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑦 ∈ V ) → ( 𝑋 ◡ E 𝑦 ↔ 𝑦 E 𝑋 ) )
6	5	elvd	⊢ ( 𝑋 ∈ 𝐵 → ( 𝑋 ◡ E 𝑦 ↔ 𝑦 E 𝑋 ) )
7		epelg	⊢ ( 𝑋 ∈ 𝐵 → ( 𝑦 E 𝑋 ↔ 𝑦 ∈ 𝑋 ) )
8	6 7	bitrd	⊢ ( 𝑋 ∈ 𝐵 → ( 𝑋 ◡ E 𝑦 ↔ 𝑦 ∈ 𝑋 ) )
9	8	abbi1dv	⊢ ( 𝑋 ∈ 𝐵 → { 𝑦 ∣ 𝑋 ◡ E 𝑦 } = 𝑋 )
10	4 9	eqtrid	⊢ ( 𝑋 ∈ 𝐵 → ( ◡ E “ { 𝑋 } ) = 𝑋 )
11	10	ineq2d	⊢ ( 𝑋 ∈ 𝐵 → ( 𝐴 ∩ ( ◡ E “ { 𝑋 } ) ) = ( 𝐴 ∩ 𝑋 ) )
12	1 11	eqtrid	⊢ ( 𝑋 ∈ 𝐵 → Pred ( E , 𝐴 , 𝑋 ) = ( 𝐴 ∩ 𝑋 ) )