Theorem fv3

Description: Alternate definition of the value of a function. Definition 6.11 of TakeutiZaring p. 26. (Contributed by NM, 30-Apr-2004) (Revised by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Assertion	fv3	⊢ ( 𝐹 ‘ 𝐴 ) = { 𝑥 ∣ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝐴 𝐹 𝑦 ) ∧ ∃! 𝑦 𝐴 𝐹 𝑦 ) }

Proof

Step	Hyp	Ref	Expression
1		elfv	⊢ ( 𝑥 ∈ ( 𝐹 ‘ 𝐴 ) ↔ ∃ 𝑧 ( 𝑥 ∈ 𝑧 ∧ ∀ 𝑦 ( 𝐴 𝐹 𝑦 ↔ 𝑦 = 𝑧 ) ) )
2		biimpr	⊢ ( ( 𝐴 𝐹 𝑦 ↔ 𝑦 = 𝑧 ) → ( 𝑦 = 𝑧 → 𝐴 𝐹 𝑦 ) )
3	2	alimi	⊢ ( ∀ 𝑦 ( 𝐴 𝐹 𝑦 ↔ 𝑦 = 𝑧 ) → ∀ 𝑦 ( 𝑦 = 𝑧 → 𝐴 𝐹 𝑦 ) )
4		breq2	⊢ ( 𝑦 = 𝑧 → ( 𝐴 𝐹 𝑦 ↔ 𝐴 𝐹 𝑧 ) )
5	4	equsalvw	⊢ ( ∀ 𝑦 ( 𝑦 = 𝑧 → 𝐴 𝐹 𝑦 ) ↔ 𝐴 𝐹 𝑧 )
6	3 5	sylib	⊢ ( ∀ 𝑦 ( 𝐴 𝐹 𝑦 ↔ 𝑦 = 𝑧 ) → 𝐴 𝐹 𝑧 )
7	6	anim2i	⊢ ( ( 𝑥 ∈ 𝑧 ∧ ∀ 𝑦 ( 𝐴 𝐹 𝑦 ↔ 𝑦 = 𝑧 ) ) → ( 𝑥 ∈ 𝑧 ∧ 𝐴 𝐹 𝑧 ) )
8	7	eximi	⊢ ( ∃ 𝑧 ( 𝑥 ∈ 𝑧 ∧ ∀ 𝑦 ( 𝐴 𝐹 𝑦 ↔ 𝑦 = 𝑧 ) ) → ∃ 𝑧 ( 𝑥 ∈ 𝑧 ∧ 𝐴 𝐹 𝑧 ) )
9		elequ2	⊢ ( 𝑧 = 𝑦 → ( 𝑥 ∈ 𝑧 ↔ 𝑥 ∈ 𝑦 ) )
10		breq2	⊢ ( 𝑧 = 𝑦 → ( 𝐴 𝐹 𝑧 ↔ 𝐴 𝐹 𝑦 ) )
11	9 10	anbi12d	⊢ ( 𝑧 = 𝑦 → ( ( 𝑥 ∈ 𝑧 ∧ 𝐴 𝐹 𝑧 ) ↔ ( 𝑥 ∈ 𝑦 ∧ 𝐴 𝐹 𝑦 ) ) )
12	11	cbvexvw	⊢ ( ∃ 𝑧 ( 𝑥 ∈ 𝑧 ∧ 𝐴 𝐹 𝑧 ) ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝐴 𝐹 𝑦 ) )
13	8 12	sylib	⊢ ( ∃ 𝑧 ( 𝑥 ∈ 𝑧 ∧ ∀ 𝑦 ( 𝐴 𝐹 𝑦 ↔ 𝑦 = 𝑧 ) ) → ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝐴 𝐹 𝑦 ) )
14		exsimpr	⊢ ( ∃ 𝑧 ( 𝑥 ∈ 𝑧 ∧ ∀ 𝑦 ( 𝐴 𝐹 𝑦 ↔ 𝑦 = 𝑧 ) ) → ∃ 𝑧 ∀ 𝑦 ( 𝐴 𝐹 𝑦 ↔ 𝑦 = 𝑧 ) )
15		eu6	⊢ ( ∃! 𝑦 𝐴 𝐹 𝑦 ↔ ∃ 𝑧 ∀ 𝑦 ( 𝐴 𝐹 𝑦 ↔ 𝑦 = 𝑧 ) )
16	14 15	sylibr	⊢ ( ∃ 𝑧 ( 𝑥 ∈ 𝑧 ∧ ∀ 𝑦 ( 𝐴 𝐹 𝑦 ↔ 𝑦 = 𝑧 ) ) → ∃! 𝑦 𝐴 𝐹 𝑦 )
17	13 16	jca	⊢ ( ∃ 𝑧 ( 𝑥 ∈ 𝑧 ∧ ∀ 𝑦 ( 𝐴 𝐹 𝑦 ↔ 𝑦 = 𝑧 ) ) → ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝐴 𝐹 𝑦 ) ∧ ∃! 𝑦 𝐴 𝐹 𝑦 ) )
18		nfeu1	⊢ Ⅎ 𝑦 ∃! 𝑦 𝐴 𝐹 𝑦
19		nfv	⊢ Ⅎ 𝑦 𝑥 ∈ 𝑧
20		nfa1	⊢ Ⅎ 𝑦 ∀ 𝑦 ( 𝐴 𝐹 𝑦 ↔ 𝑦 = 𝑧 )
21	19 20	nfan	⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝑧 ∧ ∀ 𝑦 ( 𝐴 𝐹 𝑦 ↔ 𝑦 = 𝑧 ) )
22	21	nfex	⊢ Ⅎ 𝑦 ∃ 𝑧 ( 𝑥 ∈ 𝑧 ∧ ∀ 𝑦 ( 𝐴 𝐹 𝑦 ↔ 𝑦 = 𝑧 ) )
23	18 22	nfim	⊢ Ⅎ 𝑦 ( ∃! 𝑦 𝐴 𝐹 𝑦 → ∃ 𝑧 ( 𝑥 ∈ 𝑧 ∧ ∀ 𝑦 ( 𝐴 𝐹 𝑦 ↔ 𝑦 = 𝑧 ) ) )
24		biimp	⊢ ( ( 𝐴 𝐹 𝑦 ↔ 𝑦 = 𝑧 ) → ( 𝐴 𝐹 𝑦 → 𝑦 = 𝑧 ) )
25		ax9	⊢ ( 𝑦 = 𝑧 → ( 𝑥 ∈ 𝑦 → 𝑥 ∈ 𝑧 ) )
26	24 25	syl6	⊢ ( ( 𝐴 𝐹 𝑦 ↔ 𝑦 = 𝑧 ) → ( 𝐴 𝐹 𝑦 → ( 𝑥 ∈ 𝑦 → 𝑥 ∈ 𝑧 ) ) )
27	26	impcomd	⊢ ( ( 𝐴 𝐹 𝑦 ↔ 𝑦 = 𝑧 ) → ( ( 𝑥 ∈ 𝑦 ∧ 𝐴 𝐹 𝑦 ) → 𝑥 ∈ 𝑧 ) )
28	27	sps	⊢ ( ∀ 𝑦 ( 𝐴 𝐹 𝑦 ↔ 𝑦 = 𝑧 ) → ( ( 𝑥 ∈ 𝑦 ∧ 𝐴 𝐹 𝑦 ) → 𝑥 ∈ 𝑧 ) )
29	28	anc2ri	⊢ ( ∀ 𝑦 ( 𝐴 𝐹 𝑦 ↔ 𝑦 = 𝑧 ) → ( ( 𝑥 ∈ 𝑦 ∧ 𝐴 𝐹 𝑦 ) → ( 𝑥 ∈ 𝑧 ∧ ∀ 𝑦 ( 𝐴 𝐹 𝑦 ↔ 𝑦 = 𝑧 ) ) ) )
30	29	com12	⊢ ( ( 𝑥 ∈ 𝑦 ∧ 𝐴 𝐹 𝑦 ) → ( ∀ 𝑦 ( 𝐴 𝐹 𝑦 ↔ 𝑦 = 𝑧 ) → ( 𝑥 ∈ 𝑧 ∧ ∀ 𝑦 ( 𝐴 𝐹 𝑦 ↔ 𝑦 = 𝑧 ) ) ) )
31	30	eximdv	⊢ ( ( 𝑥 ∈ 𝑦 ∧ 𝐴 𝐹 𝑦 ) → ( ∃ 𝑧 ∀ 𝑦 ( 𝐴 𝐹 𝑦 ↔ 𝑦 = 𝑧 ) → ∃ 𝑧 ( 𝑥 ∈ 𝑧 ∧ ∀ 𝑦 ( 𝐴 𝐹 𝑦 ↔ 𝑦 = 𝑧 ) ) ) )
32	15 31	syl5bi	⊢ ( ( 𝑥 ∈ 𝑦 ∧ 𝐴 𝐹 𝑦 ) → ( ∃! 𝑦 𝐴 𝐹 𝑦 → ∃ 𝑧 ( 𝑥 ∈ 𝑧 ∧ ∀ 𝑦 ( 𝐴 𝐹 𝑦 ↔ 𝑦 = 𝑧 ) ) ) )
33	23 32	exlimi	⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝐴 𝐹 𝑦 ) → ( ∃! 𝑦 𝐴 𝐹 𝑦 → ∃ 𝑧 ( 𝑥 ∈ 𝑧 ∧ ∀ 𝑦 ( 𝐴 𝐹 𝑦 ↔ 𝑦 = 𝑧 ) ) ) )
34	33	imp	⊢ ( ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝐴 𝐹 𝑦 ) ∧ ∃! 𝑦 𝐴 𝐹 𝑦 ) → ∃ 𝑧 ( 𝑥 ∈ 𝑧 ∧ ∀ 𝑦 ( 𝐴 𝐹 𝑦 ↔ 𝑦 = 𝑧 ) ) )
35	17 34	impbii	⊢ ( ∃ 𝑧 ( 𝑥 ∈ 𝑧 ∧ ∀ 𝑦 ( 𝐴 𝐹 𝑦 ↔ 𝑦 = 𝑧 ) ) ↔ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝐴 𝐹 𝑦 ) ∧ ∃! 𝑦 𝐴 𝐹 𝑦 ) )
36	1 35	bitri	⊢ ( 𝑥 ∈ ( 𝐹 ‘ 𝐴 ) ↔ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝐴 𝐹 𝑦 ) ∧ ∃! 𝑦 𝐴 𝐹 𝑦 ) )
37	36	abbi2i	⊢ ( 𝐹 ‘ 𝐴 ) = { 𝑥 ∣ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝐴 𝐹 𝑦 ) ∧ ∃! 𝑦 𝐴 𝐹 𝑦 ) }