Theorem elscottrank

Description: The rank of an element in a Scott's trick set. (Contributed by BTernaryTau, 8-Jul-2026)

	Ref	Expression
Assertion	elscottrank	|- ( A e. Scott B -> ( rank ` A ) = |^| ( rank " B ) )

Proof

Step	Hyp	Ref	Expression
1		fveqeq2	|- ( x = A -> ( ( rank ` x ) = |^| ( rank " B ) <-> ( rank ` A ) = |^| ( rank " B ) ) )
2		dfscott2	|- Scott B = { x e. B | ( rank ` x ) = |^| ( rank " B ) }
3	1 2	elrab2	|- ( A e. Scott B <-> ( A e. B /\ ( rank ` A ) = |^| ( rank " B ) ) )
4	3	simprbi	|- ( A e. Scott B -> ( rank ` A ) = |^| ( rank " B ) )