Theorem nfscott

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

	Ref	Expression
Hypothesis	nfscott.1	|- F/_ x A
Assertion	nfscott	|- F/_ x Scott A

Proof

Step	Hyp	Ref	Expression
1		nfscott.1	|- F/_ x A
2		df-scott	|- Scott A = { y e. A | A. z e. A ( rank ` y ) C_ ( rank ` z ) }
3		nfv	|- F/ x ( rank ` y ) C_ ( rank ` z )
4	1 3	nfralw	|- F/ x A. z e. A ( rank ` y ) C_ ( rank ` z )
5	4 1	nfrabw	|- F/_ x { y e. A | A. z e. A ( rank ` y ) C_ ( rank ` z ) }
6	2 5	nfcxfr	|- F/_ x Scott A