Theorem nfse

Description: Bound-variable hypothesis builder for set-like relations. (Contributed by Mario Carneiro, 24-Jun-2015) (Revised by Mario Carneiro, 14-Oct-2016)

	Ref	Expression
Hypotheses	nffr.r	|- F/_ x R
	nffr.a	|- F/_ x A
Assertion	nfse	|- F/ x R Se A

Proof

Step	Hyp	Ref	Expression
1		nffr.r	|- F/_ x R
2		nffr.a	|- F/_ x A
3		df-se	|- ( R Se A <-> A. b e. A { a e. A | a R b } e. _V )
4		nfcv	|- F/_ x a
5		nfcv	|- F/_ x b
6	4 1 5	nfbr	|- F/ x a R b
7	6 2	nfrabw	|- F/_ x { a e. A | a R b }
8	7	nfel1	|- F/ x { a e. A | a R b } e. _V
9	2 8	nfralw	|- F/ x A. b e. A { a e. A | a R b } e. _V
10	3 9	nfxfr	|- F/ x R Se A