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	⊢ Ⅎ 𝑦 𝐴
	scottexf.2	⊢ Ⅎ 𝑥 𝐴
Assertion	scottexf	⊢ { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ∈ V

Proof

Step	Hyp	Ref	Expression
1		scottexf.1	⊢ Ⅎ 𝑦 𝐴
2		scottexf.2	⊢ Ⅎ 𝑥 𝐴
3		nfcv	⊢ Ⅎ 𝑧 𝐴
4		nfv	⊢ Ⅎ 𝑧 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 )
5		nfv	⊢ Ⅎ 𝑦 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑧 )
6		fveq2	⊢ ( 𝑦 = 𝑧 → ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) )
7	6	sseq2d	⊢ ( 𝑦 = 𝑧 → ( ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ↔ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑧 ) ) )
8	1 3 4 5 7	cbvralfw	⊢ ( ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ↔ ∀ 𝑧 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑧 ) )
9	8	rabbii	⊢ { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } = { 𝑥 ∈ 𝐴 ∣ ∀ 𝑧 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑧 ) }
10		nfcv	⊢ Ⅎ 𝑤 𝐴
11		nfv	⊢ Ⅎ 𝑥 ( rank ‘ 𝑤 ) ⊆ ( rank ‘ 𝑧 )
12	2 11	nfralw	⊢ Ⅎ 𝑥 ∀ 𝑧 ∈ 𝐴 ( rank ‘ 𝑤 ) ⊆ ( rank ‘ 𝑧 )
13		nfv	⊢ Ⅎ 𝑤 ∀ 𝑧 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑧 )
14		fveq2	⊢ ( 𝑤 = 𝑥 → ( rank ‘ 𝑤 ) = ( rank ‘ 𝑥 ) )
15	14	sseq1d	⊢ ( 𝑤 = 𝑥 → ( ( rank ‘ 𝑤 ) ⊆ ( rank ‘ 𝑧 ) ↔ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑧 ) ) )
16	15	ralbidv	⊢ ( 𝑤 = 𝑥 → ( ∀ 𝑧 ∈ 𝐴 ( rank ‘ 𝑤 ) ⊆ ( rank ‘ 𝑧 ) ↔ ∀ 𝑧 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑧 ) ) )
17	10 2 12 13 16	cbvrabw	⊢ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑧 ∈ 𝐴 ( rank ‘ 𝑤 ) ⊆ ( rank ‘ 𝑧 ) } = { 𝑥 ∈ 𝐴 ∣ ∀ 𝑧 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑧 ) }
18	9 17	eqtr4i	⊢ { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } = { 𝑤 ∈ 𝐴 ∣ ∀ 𝑧 ∈ 𝐴 ( rank ‘ 𝑤 ) ⊆ ( rank ‘ 𝑧 ) }
19		scottex	⊢ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑧 ∈ 𝐴 ( rank ‘ 𝑤 ) ⊆ ( rank ‘ 𝑧 ) } ∈ V
20	18 19	eqeltri	⊢ { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ∈ V