This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqabcdv ⊢ ( 𝑋 ∈ 𝐵 → { 𝑦 ∣ 𝑋 ◡ E 𝑦 } = 𝑋 )
10 4 9 eqtrid ⊢ ( 𝑋 ∈ 𝐵 → ( ◡ E “ { 𝑋 } ) = 𝑋 )
11 10 ineq2d ⊢ ( 𝑋 ∈ 𝐵 → ( 𝐴 ∩ ( ◡ E “ { 𝑋 } ) ) = ( 𝐴 ∩ 𝑋 ) )
12 1 11 eqtrid ⊢ ( 𝑋 ∈ 𝐵 → Pred ( E , 𝐴 , 𝑋 ) = ( 𝐴 ∩ 𝑋 ) )