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	|- ( E! y A. x y = A <-> ( F/_ x A /\ A e. _V ) )

Proof

Step	Hyp	Ref	Expression
1		eusvnf	|- ( E! y A. x y = A -> F/_ x A )
2		euex	|- ( E! y A. x y = A -> E. y A. x y = A )
3		eqvisset	|- ( y = A -> A e. _V )
4	3	sps	|- ( A. x y = A -> A e. _V )
5	4	exlimiv	|- ( E. y A. x y = A -> A e. _V )
6	2 5	syl	|- ( E! y A. x y = A -> A e. _V )
7	1 6	jca	|- ( E! y A. x y = A -> ( F/_ x A /\ A e. _V ) )
8		isset	|- ( A e. _V <-> E. y y = A )
9		nfcvd	|- ( F/_ x A -> F/_ x y )
10		id	|- ( F/_ x A -> F/_ x A )
11	9 10	nfeqd	|- ( F/_ x A -> F/ x y = A )
12	11	nf5rd	|- ( F/_ x A -> ( y = A -> A. x y = A ) )
13	12	eximdv	|- ( F/_ x A -> ( E. y y = A -> E. y A. x y = A ) )
14	8 13	syl5bi	|- ( F/_ x A -> ( A e. _V -> E. y A. x y = A ) )
15	14	imp	|- ( ( F/_ x A /\ A e. _V ) -> E. y A. x y = A )
16		eusv1	|- ( E! y A. x y = A <-> E. y A. x y = A )
17	15 16	sylibr	|- ( ( F/_ x A /\ A e. _V ) -> E! y A. x y = A )
18	7 17	impbii	|- ( E! y A. x y = A <-> ( F/_ x A /\ A e. _V ) )