Metamath Proof Explorer


Theorem relexprn

Description: The range of an exponentiation of a relation a subset of the relation's field. (Contributed by RP, 23-May-2020)

Ref Expression
Assertion relexprn N 0 R V ran R r N R

Proof

Step Hyp Ref Expression
1 relexprng N 0 R V ran R r N dom R ran R
2 dmrnssfld dom R ran R R
3 1 2 sstrdi N 0 R V ran R r N R