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\in ScottB\to \mathrm{rank}\left(A\right)=\bigcap \mathrm{rank}\left[B\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)$$
4	3	simprbi	$$⊢A\in ScottB\to \mathrm{rank}\left(A\right)=\bigcap \mathrm{rank}\left[B\right]$$