Theorem fsnd 6869

Description: A singleton of an ordered pair is a function. (Contributed by AV, 17-Apr-2021.)

Hypotheses

Ref	Expression
fsnd.a	⊢ (𝜑 → 𝐴 ∈ 𝑉)
fsnd.b	⊢ (𝜑 → 𝐵 ∈ 𝑊)

Assertion

Ref	Expression
fsnd	⊢ (𝜑 → {⟨𝐴, 𝐵⟩}:{𝐴}⟶𝑊)

Proof of Theorem fsnd

Step	Hyp	Ref	Expression
1		fsnd.a	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
2		fsnd.b	. . 3 ⊢ (𝜑 → 𝐵 ∈ 𝑊)
3	1, 2	jca 521	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊))
4		f1sng 6868	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {⟨𝐴, 𝐵⟩}:{𝐴}–1-1→𝑊)
5		f1f 6778	. 2 ⊢ ({⟨𝐴, 𝐵⟩}:{𝐴}–1-1→𝑊 → {⟨𝐴, 𝐵⟩}:{𝐴}⟶𝑊)
6	3, 4, 5	3syl 19	1 ⊢ (𝜑 → {⟨𝐴, 𝐵⟩}:{𝐴}⟶𝑊)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  {csn 4584  ⟨cop 4590  ⟶wf 6534  –1-1→wf1 6535

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-mo 2565  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545

This theorem is used by:  1fv  13781  snopiswrd  14668  frgpcyg  21879  mat1dimmul  22791  pt1hmeo  24125  upgr1e  29691  1hevtxdg1  30087  wlkp1  30260  wlkl0  30968  0mplrim  34146  selvply1rhmlema  34150  selvply1rhmlemb  34151  selvply1rhmlem1  34152  selvply1rhmlem2  34153  selvply1rhmlem4  34155  selvply1rhm0  34158  evlextv  34174  reprsuc  35244  breprexplema  35259  satfv1lem  36127  frlmsnic  43604  fsetsniunop  48118  nnsum3primesprm  48887  0aryfvalel  49745  fv1arycl  49748  1arympt1fv  49750  1arymaptfo  49754