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	$$⊢\underset{\_}{Ⅎ}xB$$
Assertion	bj-seex	$$⊢\left(R\mathrm{Se}A\wedge B\in A\right)\to \left\{x\in A|xRB\right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		bj-seex.nf	$$⊢\underset{\_}{Ⅎ}xB$$
2		df-se	$$⊢R\mathrm{Se}A\leftrightarrow \forall y\in A\left\{x\in A|xRy\right\}\in \mathrm{V}$$
3	1	nfeq2	$$⊢Ⅎxy=B$$
4		breq2	$$⊢y=B\to \left(xRy\leftrightarrow xRB\right)$$
5	3 4	rabbid	$$⊢y=B\to \left\{x\in A|xRy\right\}=\left\{x\in A|xRB\right\}$$
6	5	eleq1d	$$⊢y=B\to \left(\left\{x\in A|xRy\right\}\in \mathrm{V}\leftrightarrow \left\{x\in A|xRB\right\}\in \mathrm{V}\right)$$
7	6	rspccva	$$⊢\left(\forall y\in A\left\{x\in A|xRy\right\}\in \mathrm{V}\wedge B\in A\right)\to \left\{x\in A|xRB\right\}\in \mathrm{V}$$
8	2 7	sylanb	$$⊢\left(R\mathrm{Se}A\wedge B\in A\right)\to \left\{x\in A|xRB\right\}\in \mathrm{V}$$