Theorem elscott2

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

	Ref	Expression
Assertion	elscott2	$$⊢A\in ScottB\leftrightarrow \left(A\in B\wedge \mathrm{rank}\left(A\right)=\bigcap \mathrm{rank}\left[B\right]\right)$$

Proof

Step	Hyp	Ref	Expression
1		fveqeq2	$$⊢x=A\to \left(\mathrm{rank}\left(x\right)=\bigcap \mathrm{rank}\left[B\right]\leftrightarrow \mathrm{rank}\left(A\right)=\bigcap \mathrm{rank}\left[B\right]\right)$$
2		dfscott2	$$⊢ScottB=\left\{x\in B|\mathrm{rank}\left(x\right)=\bigcap \mathrm{rank}\left[B\right]\right\}$$
3	1 2	elrab2	$$⊢A\in ScottB\leftrightarrow \left(A\in B\wedge \mathrm{rank}\left(A\right)=\bigcap \mathrm{rank}\left[B\right]\right)$$