Theorem fnmptd 6689

Description: The maps-to notation defines a function with domain. (Contributed by Glauco Siliprandi, 23-Oct-2021.)

Hypotheses

Ref	Expression
fnmptd.1	⊢ Ⅎ𝑥𝜑
fnmptd.2	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)
fnmptd.3	⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)

Assertion

Ref	Expression
fnmptd	⊢ (𝜑 → 𝐹 Fn 𝐴)

Distinct variable group:   𝑥,𝐴

Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)   𝐹(𝑥)   𝑉(𝑥)

Proof of Theorem fnmptd

Step	Hyp	Ref	Expression
1		fnmptd.1	. . 3 ⊢ Ⅎ𝑥𝜑
2		fnmptd.2	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)
3	2	ex 412	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝐵 ∈ 𝑉))
4	1, 3	ralrimi 3243	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉)
5		fnmptd.3	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
6	5	fnmpt 6688	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐹 Fn 𝐴)
7	4, 6	syl 17	1 ⊢ (𝜑 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539  Ⅎwnf 1782   ∈ wcel 2107  ∀wral 3050   ↦ cmpt 5205   Fn wfn 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pr 5412

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ral 3051  df-rex 3060  df-rab 3420  df-v 3465  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5124  df-opab 5186  df-mpt 5206  df-id 5558  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-fun 6543  df-fn 6544

This theorem is referenced by:  rngqiprngimf1  21272  elrgspnsubrunlem2  33191  nsgmgc  33375  nsgqusf1o  33379  elrspunsn  33392  ply1gsumz  33554  ply1degltdimlem  33608  evls1fldgencl  33657  ply1annidllem  33681  algextdeglem6  33702  metakunt33  42197  limsupequzmptlem  45700  liminfval2  45740  smflimmpt  46782  smflimsuplem7  46798  cfsetsnfsetfo  47030