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	$$⊢\underset{\_}{Ⅎ}xR$$
	nffr.a	$$⊢\underset{\_}{Ⅎ}xA$$
Assertion	nfse	$$⊢ℲxR\mathrm{Se}A$$

Proof

Step	Hyp	Ref	Expression
1		nffr.r	$$⊢\underset{\_}{Ⅎ}xR$$
2		nffr.a	$$⊢\underset{\_}{Ⅎ}xA$$
3		df-se	$$⊢R\mathrm{Se}A\leftrightarrow \forall b\in A\left\{a\in A|aRb\right\}\in \mathrm{V}$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}xa$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}xb$$
6	4 1 5	nfbr	$$⊢ℲxaRb$$
7	6 2	nfrabw	$$⊢\underset{\_}{Ⅎ}x\left\{a\in A|aRb\right\}$$
8	7	nfel1	$$⊢Ⅎx\left\{a\in A|aRb\right\}\in \mathrm{V}$$
9	2 8	nfralw	$$⊢Ⅎx\forall b\in A\left\{a\in A|aRb\right\}\in \mathrm{V}$$
10	3 9	nfxfr	$$⊢ℲxR\mathrm{Se}A$$