Theorem bj-seex

Description: Version of seex with a disjoint variable condition replaced by a nonfreeness hypothesis (for the sake of illustration). (Contributed by BJ, 27-Apr-2019)

	Ref	Expression
Hypothesis	bj-seex.nf	|- F/_ x B
Assertion	bj-seex	|- ( ( R Se A /\ B e. A ) -> { x e. A | x R B } e. _V )

Proof

Step	Hyp	Ref	Expression
1		bj-seex.nf	|- F/_ x B
2		df-se	|- ( R Se A <-> A. y e. A { x e. A | x R y } e. _V )
3	1	nfeq2	|- F/ x y = B
4		breq2	|- ( y = B -> ( x R y <-> x R B ) )
5	3 4	rabbid	|- ( y = B -> { x e. A | x R y } = { x e. A | x R B } )
6	5	eleq1d	|- ( y = B -> ( { x e. A | x R y } e. _V <-> { x e. A | x R B } e. _V ) )
7	6	rspccva	|- ( ( A. y e. A { x e. A | x R y } e. _V /\ B e. A ) -> { x e. A | x R B } e. _V )
8	2 7	sylanb	|- ( ( R Se A /\ B e. A ) -> { x e. A | x R B } e. _V )