Metamath Proof Explorer


Theorem elrtrclrec

Description: Membership in the indexed union of relation exponentiation over the natural numbers (including zero) is equivalent to the existence of at least one number such that the element is a member of that relationship power. (Contributed by RP, 2-Jun-2020)

Ref Expression
Hypothesis rtrclrec.def C = r V n 0 r r n
Assertion elrtrclrec R V X C R n 0 X R r n

Proof

Step Hyp Ref Expression
1 rtrclrec.def C = r V n 0 r r n
2 nn0ex 0 V
3 1 eliunov2 R V 0 V X C R n 0 X R r n
4 2 3 mpan2 R V X C R n 0 X R r n