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 
|- ( X e. B -> Pred ( _E , A , X ) = ( A i^i X ) )

Proof

Step Hyp Ref Expression
1 df-pred 
 |-  Pred ( _E , A , X ) = ( A i^i ( `' _E " { X } ) )
2 relcnv 
 |-  Rel `' _E
3 relimasn 
 |-  ( Rel `' _E -> ( `' _E " { X } ) = { y | X `' _E y } )
4 2 3 ax-mp 
 |-  ( `' _E " { X } ) = { y | X `' _E y }
5 brcnvg 
 |-  ( ( X e. B /\ y e. _V ) -> ( X `' _E y <-> y _E X ) )
6 5 elvd 
 |-  ( X e. B -> ( X `' _E y <-> y _E X ) )
7 epelg 
 |-  ( X e. B -> ( y _E X <-> y e. X ) )
8 6 7 bitrd 
 |-  ( X e. B -> ( X `' _E y <-> y e. X ) )
9 8 eqabcdv 
 |-  ( X e. B -> { y | X `' _E y } = X )
10 4 9 eqtrid 
 |-  ( X e. B -> ( `' _E " { X } ) = X )
11 10 ineq2d 
 |-  ( X e. B -> ( A i^i ( `' _E " { X } ) ) = ( A i^i X ) )
12 1 11 eqtrid 
 |-  ( X e. B -> Pred ( _E , A , X ) = ( A i^i X ) )