Metamath Proof Explorer


Theorem 0setrec

Description: If a function sends the empty set to itself, the function will not recursively generate any sets, regardless of its other values. (Contributed by Emmett Weisz, 23-Jun-2021)

Ref Expression
Hypothesis 0setrec.1 φ F =
Assertion 0setrec φ setrecs F =

Proof

Step Hyp Ref Expression
1 0setrec.1 φ F =
2 eqid setrecs F = setrecs F
3 ss0 x x =
4 fveq2 x = F x = F
5 4 1 sylan9eqr φ x = F x =
6 5 ex φ x = F x =
7 eqimss F x = F x
8 3 6 7 syl56 φ x F x
9 8 alrimiv φ x x F x
10 2 9 setrec2v φ setrecs F
11 ss0 setrecs F setrecs F =
12 10 11 syl φ setrecs F =