Metamath Proof Explorer

Theorem zs12ex

Description: The class of dyadic fractions is a set. (Contributed by Scott Fenton, 7-Aug-2025)

Ref Expression
Assertion zs12ex 
|- ZZ_s[1/2] e. _V

Proof

Step Hyp Ref Expression
1 df-zs12 
 |-  ZZ_s[1/2] = { x | E. y e. ZZ_s E. z e. NN0_s x = ( y /su ( 2s ^su z ) ) }
2 zsex 
 |-  ZZ_s e. _V
3 n0sex 
 |-  NN0_s e. _V
4 2 3 ab2rexex 
 |-  { x | E. y e. ZZ_s E. z e. NN0_s x = ( y /su ( 2s ^su z ) ) } e. _V
5 1 4 eqeltri 
 |-  ZZ_s[1/2] e. _V