Theorem elsetrecs

Description: A set A is an element of setrecs ( F ) iff A is generated by some subset of setrecs ( F ) . The proof requires both setrec1 and setrec2 , but this theorem is not strong enough to uniquely determine setrecs ( F ) . If F respects the subset relation, the theorem still holds if both occurrences of e. are replaced by C_ for a stronger version of the theorem. (Contributed by Emmett Weisz, 12-Jul-2021)

	Ref	Expression
Hypothesis	elsetrecs.1	|- B = setrecs ( F )
Assertion	elsetrecs	|- ( A e. B <-> E. x ( x C_ B /\ A e. ( F ` x ) ) )

Proof

Step	Hyp	Ref	Expression
1		elsetrecs.1	|- B = setrecs ( F )
2	1	elsetrecslem	|- ( A e. B -> E. x ( x C_ B /\ A e. ( F ` x ) ) )
3		vex	|- x e. _V
4	3	a1i	|- ( x C_ B -> x e. _V )
5		id	|- ( x C_ B -> x C_ B )
6	1 4 5	setrec1	|- ( x C_ B -> ( F ` x ) C_ B )
7	6	sselda	|- ( ( x C_ B /\ A e. ( F ` x ) ) -> A e. B )
8	7	exlimiv	|- ( E. x ( x C_ B /\ A e. ( F ` x ) ) -> A e. B )
9	2 8	impbii	|- ( A e. B <-> E. x ( x C_ B /\ A e. ( F ` x ) ) )