Theorem scottab

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

	Ref	Expression
Hypothesis	scottab.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion	scottab	⊢ Scott { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ ( 𝜑 ∧ ∀ 𝑦 ( 𝜓 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) }

Proof

Step	Hyp	Ref	Expression
1		scottab.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2		nfv	⊢ Ⅎ 𝑥 𝜓
3	2 1	scottabf	⊢ Scott { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ ( 𝜑 ∧ ∀ 𝑦 ( 𝜓 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) }