Metamath Proof Explorer

Theorem elscott2

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

Ref Expression
Assertion elscott2 
|- ( A e. Scott B <-> ( A e. 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 ) ) )