Theorem elscott

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

	Ref	Expression
Assertion	elscott	|- ( A e. Scott B <-> ( A e. B /\ A. x e. B ( rank ` A ) C_ ( rank ` x ) ) )

Proof

Step	Hyp	Ref	Expression
1		fveq2	|- ( y = A -> ( rank ` y ) = ( rank ` A ) )
2	1	sseq1d	|- ( y = A -> ( ( rank ` y ) C_ ( rank ` x ) <-> ( rank ` A ) C_ ( rank ` x ) ) )
3	2	ralbidv	|- ( y = A -> ( A. x e. B ( rank ` y ) C_ ( rank ` x ) <-> A. x e. B ( rank ` A ) C_ ( rank ` x ) ) )
4		df-scott	|- Scott B = { y e. B | A. x e. B ( rank ` y ) C_ ( rank ` x ) }
5	3 4	elrab2	|- ( A e. Scott B <-> ( A e. B /\ A. x e. B ( rank ` A ) C_ ( rank ` x ) ) )