Theorem fnopabfv 2858

Description: Representation of a function in terms of its values.

Assertion

Ref	Expression
fnopabfv	⊢ (F Fn A ↔ F = {⟨x, y⟩∣(x ∈ A ∧ y = (F ‘x))})

Distinct variable group(s):   x,y,A   x,F,y

Proof of Theorem fnopabfv

Step	Hyp	Ref	Expression
1		visset 1350	. . . . . . . . 9 ⊢ z ∈ V
2		visset 1350	. . . . . . . . 9 ⊢ w ∈ V
3	1, 2	fnop 2727	. . . . . . . 8 ⊢ ((F Fn A ∧ ⟨z, w⟩ ∈ F) → z ∈ A)
4	3	exp 291	. . . . . . 7 ⊢ (F Fn A → (⟨z, w⟩ ∈ F → z ∈ A))
5		pm4.71r 482	. . . . . . 7 ⊢ ((⟨z, w⟩ ∈ F → z ∈ A) ↔ (⟨z, w⟩ ∈ F ↔ (z ∈ A ∧ ⟨z, w⟩ ∈ F)))
6	4, 5	sylib 173	. . . . . 6 ⊢ (F Fn A → (⟨z, w⟩ ∈ F ↔ (z ∈ A ∧ ⟨z, w⟩ ∈ F)))
7	2	fnfvop 2856	. . . . . . . . 9 ⊢ ((F Fn A ∧ z ∈ A) → ((F ‘z) = w ↔ ⟨z, w⟩ ∈ F))
8		cleqcom 1103	. . . . . . . . 9 ⊢ (w = (F ‘z) ↔ (F ‘z) = w)
9	7, 8	syl5bb 410	. . . . . . . 8 ⊢ ((F Fn A ∧ z ∈ A) → (w = (F ‘z) ↔ ⟨z, w⟩ ∈ F))
10	9	exp 291	. . . . . . 7 ⊢ (F Fn A → (z ∈ A → (w = (F ‘z) ↔ ⟨z, w⟩ ∈ F)))
11	10	pm5.32d 491	. . . . . 6 ⊢ (F Fn A → ((z ∈ A ∧ w = (F ‘z)) ↔ (z ∈ A ∧ ⟨z, w⟩ ∈ F)))
12	6, 11	bitr4d 409	. . . . 5 ⊢ (F Fn A → (⟨z, w⟩ ∈ F ↔ (z ∈ A ∧ w = (F ‘z))))
13		eleq1 1149	. . . . . . 7 ⊢ (x = z → (x ∈ A ↔ z ∈ A))
14		fveq2 2832	. . . . . . . 8 ⊢ (x = z → (F ‘x) = (F ‘z))
15	14	cleq2d 1112	. . . . . . 7 ⊢ (x = z → (y = (F ‘x) ↔ y = (F ‘z)))
16	13, 15	anbi12d 476	. . . . . 6 ⊢ (x = z → ((x ∈ A ∧ y = (F ‘x)) ↔ (z ∈ A ∧ y = (F ‘z))))
17		cleq1 1107	. . . . . . 7 ⊢ (y = w → (y = (F ‘z) ↔ w = (F ‘z)))
18	17	anbi2d 468	. . . . . 6 ⊢ (y = w → ((z ∈ A ∧ y = (F ‘z)) ↔ (z ∈ A ∧ w = (F ‘z))))
19	1, 2, 16, 18	opelopab 2117	. . . . 5 ⊢ (⟨z, w⟩ ∈ {⟨x, y⟩∣(x ∈ A ∧ y = (F ‘x))} ↔ (z ∈ A ∧ w = (F ‘z)))
20	12, 19	syl6bbr 416	. . . 4 ⊢ (F Fn A → (⟨z, w⟩ ∈ F ↔ ⟨z, w⟩ ∈ {⟨x, y⟩∣(x ∈ A ∧ y = (F ‘x))}))
21	20	19.21aivv 944	. . 3 ⊢ (F Fn A → ∀z∀w(⟨z, w⟩ ∈ F ↔ ⟨z, w⟩ ∈ {⟨x, y⟩∣(x ∈ A ∧ y = (F ‘x))}))
22		fnrel 2722	. . . . 5 ⊢ (F Fn A → Rel F)
23		relopab 2494	. . . . 5 ⊢ Rel {⟨x, y⟩∣(x ∈ A ∧ y = (F ‘x))}
24	22, 23	jctir 241	. . . 4 ⊢ (F Fn A → (Rel F ∧ Rel {⟨x, y⟩∣(x ∈ A ∧ y = (F ‘x))}))
25		cleqrel 2483	. . . 4 ⊢ ((Rel F ∧ Rel {⟨x, y⟩∣(x ∈ A ∧ y = (F ‘x))}) → (F = {⟨x, y⟩∣(x ∈ A ∧ y = (F ‘x))} ↔ ∀z∀w(⟨z, w⟩ ∈ F ↔ ⟨z, w⟩ ∈ {⟨x, y⟩∣(x ∈ A ∧ y = (F ‘x))})))
26	24, 25	syl 12	. . 3 ⊢ (F Fn A → (F = {⟨x, y⟩∣(x ∈ A ∧ y = (F ‘x))} ↔ ∀z∀w(⟨z, w⟩ ∈ F ↔ ⟨z, w⟩ ∈ {⟨x, y⟩∣(x ∈ A ∧ y = (F ‘x))})))
27	21, 26	mpbird 171	. 2 ⊢ (F Fn A → F = {⟨x, y⟩∣(x ∈ A ∧ y = (F ‘x))})
28		fvex 2838	. . . 4 ⊢ (F ‘x) ∈ V
29		cleqid 1102	. . . 4 ⊢ {⟨x, y⟩∣(x ∈ A ∧ y = (F ‘x))} = {⟨x, y⟩∣(x ∈ A ∧ y = (F ‘x))}
30	28, 29	fnopab2 2747	. . 3 ⊢ {⟨x, y⟩∣(x ∈ A ∧ y = (F ‘x))} Fn A
31		fneq1 2718	. . 3 ⊢ (F = {⟨x, y⟩∣(x ∈ A ∧ y = (F ‘x))} → (F Fn A ↔ {⟨x, y⟩∣(x ∈ A ∧ y = (F ‘x))} Fn A))
32	30, 31	mpbiri 169	. 2 ⊢ (F = {⟨x, y⟩∣(x ∈ A ∧ y = (F ‘x))} → F Fn A)
33	27, 32	impbi 139	1 ⊢ (F Fn A ↔ F = {⟨x, y⟩∣(x ∈ A ∧ y = (F ‘x))})

Syntax hints:   → wi 2   ↔ wb 127   ∧ wa 196  ∀wal 672   = weq 797   = wceq 1091   ∈ wcel 1092  ⟨cop 1810  {copab 2055  Rel wrel 2415   Fn wfn 2417   ‘cfv 2422

This theorem is referenced by:  fopabfv 2894  fnoprval 3042  xpmapenlem3 3393  pjrn 5587

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-uni 1920  df-br 2063  df-opab 2098  df-id 2125  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-fv 2438

metamath.org