Theorem elright

Description: Membership in the right set of a surreal. (Contributed by Scott Fenton, 7-Nov-2025)

	Ref	Expression
Assertion	elright	$$⊢A\in R\left(B\right)\leftrightarrow \left(A\in \mathrm{Old}\left(\mathrm{bday}\left(B\right)\right)\wedge B{<}_{s}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		breq2	$$⊢x=A\to \left(B{<}_{s}x\leftrightarrow B{<}_{s}A\right)$$
2		rightval	$$⊢R\left(B\right)=\left\{x\in \mathrm{Old}\left(\mathrm{bday}\left(B\right)\right)|B{<}_{s}x\right\}$$
3	1 2	elrab2	$$⊢A\in R\left(B\right)\leftrightarrow \left(A\in \mathrm{Old}\left(\mathrm{bday}\left(B\right)\right)\wedge B{<}_{s}A\right)$$