Metamath Proof Explorer

Theorem reldmevls1

Description: Well-behaved binary operation property of evalSub1 . (Contributed by AV, 7-Sep-2019)

Ref Expression
Assertion reldmevls1 
|- Rel dom evalSub1

Proof

Step Hyp Ref Expression
1 df-evls1 
 |-  evalSub1 = ( s e. _V , r e. ~P ( Base ` s ) |-> [_ ( Base ` s ) / b ]_ ( ( x e. ( b ^m ( b ^m 1o ) ) |-> ( x o. ( y e. b |-> ( 1o X. { y } ) ) ) ) o. ( ( 1o evalSub s ) ` r ) ) )
2 1 reldmmpo 
 |-  Rel dom evalSub1