Theorem scottexf

Description: A version of scottex with nonfree variables instead of distinct variables. (Contributed by Giovanni Mascellani, 19-Aug-2018)

	Ref	Expression
Hypotheses	scottexf.1	|- F/_ y A
	scottexf.2	|- F/_ x A
Assertion	scottexf	|- { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } e. _V

Proof

Step	Hyp	Ref	Expression
1		scottexf.1	|- F/_ y A
2		scottexf.2	|- F/_ x A
3		nfcv	|- F/_ z A
4		nfv	|- F/ z ( rank ` x ) C_ ( rank ` y )
5		nfv	|- F/ y ( rank ` x ) C_ ( rank ` z )
6		fveq2	|- ( y = z -> ( rank ` y ) = ( rank ` z ) )
7	6	sseq2d	|- ( y = z -> ( ( rank ` x ) C_ ( rank ` y ) <-> ( rank ` x ) C_ ( rank ` z ) ) )
8	1 3 4 5 7	cbvralfw	|- ( A. y e. A ( rank ` x ) C_ ( rank ` y ) <-> A. z e. A ( rank ` x ) C_ ( rank ` z ) )
9	8	rabbii	|- { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } = { x e. A | A. z e. A ( rank ` x ) C_ ( rank ` z ) }
10		nfcv	|- F/_ w A
11		nfv	|- F/ x ( rank ` w ) C_ ( rank ` z )
12	2 11	nfralw	|- F/ x A. z e. A ( rank ` w ) C_ ( rank ` z )
13		nfv	|- F/ w A. z e. A ( rank ` x ) C_ ( rank ` z )
14		fveq2	|- ( w = x -> ( rank ` w ) = ( rank ` x ) )
15	14	sseq1d	|- ( w = x -> ( ( rank ` w ) C_ ( rank ` z ) <-> ( rank ` x ) C_ ( rank ` z ) ) )
16	15	ralbidv	|- ( w = x -> ( A. z e. A ( rank ` w ) C_ ( rank ` z ) <-> A. z e. A ( rank ` x ) C_ ( rank ` z ) ) )
17	10 2 12 13 16	cbvrabw	|- { w e. A | A. z e. A ( rank ` w ) C_ ( rank ` z ) } = { x e. A | A. z e. A ( rank ` x ) C_ ( rank ` z ) }
18	9 17	eqtr4i	|- { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } = { w e. A | A. z e. A ( rank ` w ) C_ ( rank ` z ) }
19		scottex	|- { w e. A | A. z e. A ( rank ` w ) C_ ( rank ` z ) } e. _V
20	18 19	eqeltri	|- { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } e. _V