Metamath Proof Explorer


Theorem nfscott

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

Ref Expression
Hypothesis nfscott.1 _ x A
Assertion nfscott _ x Scott A

Proof

Step Hyp Ref Expression
1 nfscott.1 _ x A
2 df-scott Scott A = y A | z A rank y rank z
3 nfv x rank y rank z
4 1 3 nfralw x z A rank y rank z
5 4 1 nfrabw _ x y A | z A rank y rank z
6 2 5 nfcxfr _ x Scott A