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	⊢ ( ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑦 𝑥 𝐹 𝑦 } ) ‘ 𝑎 ) = ( 𝐹 ‘ 𝑎 )

Proof

Step	Hyp	Ref	Expression
1		fvres	⊢ ( 𝑎 ∈ { 𝑥 ∣ ∃! 𝑦 𝑥 𝐹 𝑦 } → ( ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑦 𝑥 𝐹 𝑦 } ) ‘ 𝑎 ) = ( 𝐹 ‘ 𝑎 ) )
2		nfvres	⊢ ( ¬ 𝑎 ∈ { 𝑥 ∣ ∃! 𝑦 𝑥 𝐹 𝑦 } → ( ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑦 𝑥 𝐹 𝑦 } ) ‘ 𝑎 ) = ∅ )
3		vex	⊢ 𝑎 ∈ V
4		breq1	⊢ ( 𝑥 = 𝑎 → ( 𝑥 𝐹 𝑦 ↔ 𝑎 𝐹 𝑦 ) )
5	4	eubidv	⊢ ( 𝑥 = 𝑎 → ( ∃! 𝑦 𝑥 𝐹 𝑦 ↔ ∃! 𝑦 𝑎 𝐹 𝑦 ) )
6	3 5	elab	⊢ ( 𝑎 ∈ { 𝑥 ∣ ∃! 𝑦 𝑥 𝐹 𝑦 } ↔ ∃! 𝑦 𝑎 𝐹 𝑦 )
7		tz6.12-2	⊢ ( ¬ ∃! 𝑦 𝑎 𝐹 𝑦 → ( 𝐹 ‘ 𝑎 ) = ∅ )
8	6 7	sylnbi	⊢ ( ¬ 𝑎 ∈ { 𝑥 ∣ ∃! 𝑦 𝑥 𝐹 𝑦 } → ( 𝐹 ‘ 𝑎 ) = ∅ )
9	2 8	eqtr4d	⊢ ( ¬ 𝑎 ∈ { 𝑥 ∣ ∃! 𝑦 𝑥 𝐹 𝑦 } → ( ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑦 𝑥 𝐹 𝑦 } ) ‘ 𝑎 ) = ( 𝐹 ‘ 𝑎 ) )
10	1 9	pm2.61i	⊢ ( ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑦 𝑥 𝐹 𝑦 } ) ‘ 𝑎 ) = ( 𝐹 ‘ 𝑎 )