Theorem scottabes

Description: Value of the Scott operation at a class abstraction. Variant of scottab using explicit substitution. (Contributed by Rohan Ridenour, 14-Aug-2023)

	Ref	Expression
Assertion	scottabes	⊢ Scott { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ ( 𝜑 ∧ ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) }

Proof

Step	Hyp	Ref	Expression
1		nfs1v	⊢ Ⅎ 𝑥 [ 𝑦 / 𝑥 ] 𝜑
2		sbequ12	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) )
3	1 2	scottabf	⊢ Scott { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ ( 𝜑 ∧ ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) }