Metamath Proof Explorer


Theorem elrnust

Description: First direction for ustbas . (Contributed by Thierry Arnoux, 16-Nov-2017)

Ref Expression
Assertion elrnust UUnifOnXUranUnifOn

Proof

Step Hyp Ref Expression
1 elfvdm UUnifOnXXdomUnifOn
2 fveq2 x=XUnifOnx=UnifOnX
3 2 eleq2d x=XUUnifOnxUUnifOnX
4 3 rspcev XdomUnifOnUUnifOnXxdomUnifOnUUnifOnx
5 1 4 mpancom UUnifOnXxdomUnifOnUUnifOnx
6 ustfn UnifOnFnV
7 fnfun UnifOnFnVFunUnifOn
8 elunirn FunUnifOnUranUnifOnxdomUnifOnUUnifOnx
9 6 7 8 mp2b UranUnifOnxdomUnifOnUUnifOnx
10 5 9 sylibr UUnifOnXUranUnifOn