MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ixpfn Structured version   Visualization version   GIF version

Theorem ixpfn 8944
Description: A nuple is a function. (Contributed by FL, 6-Jun-2011.) (Revised by Mario Carneiro, 31-May-2014.)
Assertion
Ref Expression
ixpfn (𝐹X𝑥𝐴 𝐵𝐹 Fn 𝐴)
Distinct variable group:   𝑥,𝐴
Allowed substitution hints:   𝐵(𝑥)   𝐹(𝑥)

Proof of Theorem ixpfn
Dummy variable 𝑓 is distinct from all other variables.
StepHypRef Expression
1 fneq1 6658 . 2 (𝑓 = 𝐹 → (𝑓 Fn 𝐴𝐹 Fn 𝐴))
2 elixp2 8942 . . 3 (𝑓X𝑥𝐴 𝐵 ↔ (𝑓 ∈ V ∧ 𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵))
32simp2bi 1146 . 2 (𝑓X𝑥𝐴 𝐵𝑓 Fn 𝐴)
41, 3vtoclga 3576 1 (𝐹X𝑥𝐴 𝐵𝐹 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  wral 3060  Vcvv 3479   Fn wfn 6555  cfv 6560  Xcixp 8938
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-ext 2707
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-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ral 3061  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-opab 5205  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-iota 6513  df-fun 6562  df-fn 6563  df-fv 6568  df-ixp 8939
This theorem is referenced by:  ixpprc  8960  undifixp  8975  resixpfo  8977  boxcutc  8982  ixpiunwdom  9631  prdsbasfn  17517  xpsff1o  17613  sscfn1  17862  funcfn2  17915  natfn  18003  pthaus  23647  ptuncnv  23816  ptunhmeo  23817  ptcmplem2  24062  prdsbl  24505  finixpnum  37613  upixp  37737  prdstotbnd  37802  elixpconstg  45099  rrxsnicc  46320  ioorrnopnxrlem  46326  hoidmvlelem3  46617  hspdifhsp  46636  hspmbllem2  46647
  Copyright terms: Public domain W3C validator