Theorem elscott2

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

	Ref	Expression
Assertion	elscott2	⊢ ( 𝐴 ∈ Scott 𝐵 ↔ ( 𝐴 ∈ 𝐵 ∧ ( rank ‘ 𝐴 ) = ∩ ( rank “ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fveqeq2	⊢ ( 𝑥 = 𝐴 → ( ( rank ‘ 𝑥 ) = ∩ ( rank “ 𝐵 ) ↔ ( rank ‘ 𝐴 ) = ∩ ( rank “ 𝐵 ) ) )
2		dfscott2	⊢ Scott 𝐵 = { 𝑥 ∈ 𝐵 ∣ ( rank ‘ 𝑥 ) = ∩ ( rank “ 𝐵 ) }
3	1 2	elrab2	⊢ ( 𝐴 ∈ Scott 𝐵 ↔ ( 𝐴 ∈ 𝐵 ∧ ( rank ‘ 𝐴 ) = ∩ ( rank “ 𝐵 ) ) )