Theorem elscott

Description: Membership in a Scott's trick set. (Contributed by BTernaryTau, 3-Jul-2026)

	Ref	Expression
Assertion	elscott	⊢ ( 𝐴 ∈ Scott 𝐵 ↔ ( 𝐴 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝑦 = 𝐴 → ( rank ‘ 𝑦 ) = ( rank ‘ 𝐴 ) )
2	1	sseq1d	⊢ ( 𝑦 = 𝐴 → ( ( rank ‘ 𝑦 ) ⊆ ( rank ‘ 𝑥 ) ↔ ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝑥 ) ) )
3	2	ralbidv	⊢ ( 𝑦 = 𝐴 → ( ∀ 𝑥 ∈ 𝐵 ( rank ‘ 𝑦 ) ⊆ ( rank ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐵 ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝑥 ) ) )
4		df-scott	⊢ Scott 𝐵 = { 𝑦 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝐵 ( rank ‘ 𝑦 ) ⊆ ( rank ‘ 𝑥 ) }
5	3 4	elrab2	⊢ ( 𝐴 ∈ Scott 𝐵 ↔ ( 𝐴 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝑥 ) ) )