Metamath Proof Explorer


Theorem setrec2lem1

Description: Lemma for setrec2 . The functional part of F has the same values as F . (Contributed by Emmett Weisz, 4-Mar-2021) (New usage is discouraged.)

Ref Expression
Assertion setrec2lem1 Fx|∃!yxFya=Fa

Proof

Step Hyp Ref Expression
1 fvres ax|∃!yxFyFx|∃!yxFya=Fa
2 nfvres ¬ax|∃!yxFyFx|∃!yxFya=
3 vex aV
4 breq1 x=axFyaFy
5 4 eubidv x=a∃!yxFy∃!yaFy
6 3 5 elab ax|∃!yxFy∃!yaFy
7 tz6.12-2 ¬∃!yaFyFa=
8 6 7 sylnbi ¬ax|∃!yxFyFa=
9 2 8 eqtr4d ¬ax|∃!yxFyFx|∃!yxFya=Fa
10 1 9 pm2.61i Fx|∃!yxFya=Fa