Theorem bnj93

Description: Technical lemma for bnj97 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		df-bnj15	|- ( R _FrSe A <-> ( R Fr A /\ R _Se A ) )
2	1	simprbi	|- ( R _FrSe A -> R _Se A )
3		df-bnj13	|- ( R _Se A <-> A. x e. A _pred ( x , A , R ) e. _V )
4	2 3	sylib	|- ( R _FrSe A -> A. x e. A _pred ( x , A , R ) e. _V )
5	4	r19.21bi	|- ( ( R _FrSe A /\ x e. A ) -> _pred ( x , A , R ) e. _V )