Metamath Proof Explorer


Theorem exrecfn

Description: Theorem about the existence of infinite recursive sets. y should usually be free in B . (Contributed by ML, 30-Mar-2022)

Ref Expression
Assertion exrecfn A V y B W x A x y x B x

Proof

Step Hyp Ref Expression
1 eqid z V z ran y z B = z V z ran y z B
2 1 exrecfnlem A V y B W x A x y x B x