Theorem eusvnfb

Description: Two ways to say that A ( x ) is a set expression that does not depend on x . (Contributed by Mario Carneiro, 18-Nov-2016)

	Ref	Expression
Assertion	eusvnfb	$$⊢\exists !y\forall xy=A\leftrightarrow \left(\underset{\_}{Ⅎ}xA\wedge A\in \mathrm{V}\right)$$

Proof

Step	Hyp	Ref	Expression
1		eusvnf	$$⊢\exists !y\forall xy=A\to \underset{\_}{Ⅎ}xA$$
2		euex	$$⊢\exists !y\forall xy=A\to \exists y\forall xy=A$$
3		eqvisset	$$⊢y=A\to A\in \mathrm{V}$$
4	3	sps	$$⊢\forall xy=A\to A\in \mathrm{V}$$
5	4	exlimiv	$$⊢\exists y\forall xy=A\to A\in \mathrm{V}$$
6	2 5	syl	$$⊢\exists !y\forall xy=A\to A\in \mathrm{V}$$
7	1 6	jca	$$⊢\exists !y\forall xy=A\to \left(\underset{\_}{Ⅎ}xA\wedge A\in \mathrm{V}\right)$$
8		isset	$$⊢A\in \mathrm{V}\leftrightarrow \exists yy=A$$
9		nfcvd	$$⊢\underset{\_}{Ⅎ}xA\to \underset{\_}{Ⅎ}xy$$
10		id	$$⊢\underset{\_}{Ⅎ}xA\to \underset{\_}{Ⅎ}xA$$
11	9 10	nfeqd	$$⊢\underset{\_}{Ⅎ}xA\to Ⅎxy=A$$
12	11	nf5rd	$$⊢\underset{\_}{Ⅎ}xA\to \left(y=A\to \forall xy=A\right)$$
13	12	eximdv	$$⊢\underset{\_}{Ⅎ}xA\to \left(\exists yy=A\to \exists y\forall xy=A\right)$$
14	8 13	biimtrid	$$⊢\underset{\_}{Ⅎ}xA\to \left(A\in \mathrm{V}\to \exists y\forall xy=A\right)$$
15	14	imp	$$⊢\left(\underset{\_}{Ⅎ}xA\wedge A\in \mathrm{V}\right)\to \exists y\forall xy=A$$
16		eusv1	$$⊢\exists !y\forall xy=A\leftrightarrow \exists y\forall xy=A$$
17	15 16	sylibr	$$⊢\left(\underset{\_}{Ⅎ}xA\wedge A\in \mathrm{V}\right)\to \exists !y\forall xy=A$$
18	7 17	impbii	$$⊢\exists !y\forall xy=A\leftrightarrow \left(\underset{\_}{Ⅎ}xA\wedge A\in \mathrm{V}\right)$$