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

Metamath Proof Explorer

Theorem bnj1148

Description: Property of _pred . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Assertion bnj1148 
|- ( ( R _FrSe A /\ X e. A ) -> _pred ( X , A , R ) e. _V )

Proof

Step Hyp Ref Expression
1 elisset 
 |-  ( X e. A -> E. x x = X )
2 1 adantl 
 |-  ( ( R _FrSe A /\ X e. A ) -> E. x x = X )
3 bnj93 
 |-  ( ( R _FrSe A /\ x e. A ) -> _pred ( x , A , R ) e. _V )
4 eleq1 
 |-  ( x = X -> ( x e. A <-> X e. A ) )
5 4 anbi2d 
 |-  ( x = X -> ( ( R _FrSe A /\ x e. A ) <-> ( R _FrSe A /\ X e. A ) ) )
6 bnj602 
 |-  ( x = X -> _pred ( x , A , R ) = _pred ( X , A , R ) )
7 6 eleq1d 
 |-  ( x = X -> ( _pred ( x , A , R ) e. _V <-> _pred ( X , A , R ) e. _V ) )
8 5 7 imbi12d 
 |-  ( x = X -> ( ( ( R _FrSe A /\ x e. A ) -> _pred ( x , A , R ) e. _V ) <-> ( ( R _FrSe A /\ X e. A ) -> _pred ( X , A , R ) e. _V ) ) )
9 3 8 mpbii 
 |-  ( x = X -> ( ( R _FrSe A /\ X e. A ) -> _pred ( X , A , R ) e. _V ) )
10 2 9 bnj593 
 |-  ( ( R _FrSe A /\ X e. A ) -> E. x ( ( R _FrSe A /\ X e. A ) -> _pred ( X , A , R ) e. _V ) )
11 10 bnj937 
 |-  ( ( R _FrSe A /\ X e. A ) -> ( ( R _FrSe A /\ X e. A ) -> _pred ( X , A , R ) e. _V ) )
12 11 pm2.43i 
 |-  ( ( R _FrSe A /\ X e. A ) -> _pred ( X , A , R ) e. _V )