Metamath Proof Explorer
Description: Version of setrec2 with a disjoint variable condition instead of a
non-freeness hypothesis. (Contributed by Emmett Weisz, 6-Mar-2021)
|
|
Ref |
Expression |
|
Hypotheses |
setrec2.b |
⊢ 𝐵 = setrecs ( 𝐹 ) |
|
|
setrec2.c |
⊢ ( 𝜑 → ∀ 𝑎 ( 𝑎 ⊆ 𝐶 → ( 𝐹 ‘ 𝑎 ) ⊆ 𝐶 ) ) |
|
Assertion |
setrec2v |
⊢ ( 𝜑 → 𝐵 ⊆ 𝐶 ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
setrec2.b |
⊢ 𝐵 = setrecs ( 𝐹 ) |
2 |
|
setrec2.c |
⊢ ( 𝜑 → ∀ 𝑎 ( 𝑎 ⊆ 𝐶 → ( 𝐹 ‘ 𝑎 ) ⊆ 𝐶 ) ) |
3 |
|
nfcv |
⊢ Ⅎ 𝑎 𝐹 |
4 |
3 1 2
|
setrec2 |
⊢ ( 𝜑 → 𝐵 ⊆ 𝐶 ) |