Theorem nfscott

Description: Bound-variable hypothesis builder for the Scott operation. (Contributed by Rohan Ridenour, 11-Aug-2023)

	Ref	Expression
Hypothesis	nfscott.1	⊢ Ⅎ 𝑥 𝐴
Assertion	nfscott	⊢ Ⅎ 𝑥 Scott 𝐴

Proof

Step	Hyp	Ref	Expression
1		nfscott.1	⊢ Ⅎ 𝑥 𝐴
2		df-scott	⊢ Scott 𝐴 = { 𝑦 ∈ 𝐴 ∣ ∀ 𝑧 ∈ 𝐴 ( rank ‘ 𝑦 ) ⊆ ( rank ‘ 𝑧 ) }
3		nfv	⊢ Ⅎ 𝑥 ( rank ‘ 𝑦 ) ⊆ ( rank ‘ 𝑧 )
4	1 3	nfralw	⊢ Ⅎ 𝑥 ∀ 𝑧 ∈ 𝐴 ( rank ‘ 𝑦 ) ⊆ ( rank ‘ 𝑧 )
5	4 1	nfrabw	⊢ Ⅎ 𝑥 { 𝑦 ∈ 𝐴 ∣ ∀ 𝑧 ∈ 𝐴 ( rank ‘ 𝑦 ) ⊆ ( rank ‘ 𝑧 ) }
6	2 5	nfcxfr	⊢ Ⅎ 𝑥 Scott 𝐴