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 e. V /\ A. y B e. W ) -> E. x ( A C_ x /\ A. y e. x B e. x ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( z e. _V |-> ( z u. ran ( y e. z |-> B ) ) ) = ( z e. _V |-> ( z u. ran ( y e. z |-> B ) ) )
2	1	exrecfnlem	|- ( ( A e. V /\ A. y B e. W ) -> E. x ( A C_ x /\ A. y e. x B e. x ) )