Metamath Proof Explorer

Theorem setrec2v

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 B = setrecs F
setrec2.c φ a a C F a C
Assertion setrec2v φ B C


Step Hyp Ref Expression
1 setrec2.b B = setrecs F
2 setrec2.c φ a a C F a C
3 nfcv _ a F
4 3 1 2 setrec2 φ B C