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

Theorem ixpfn 8452
 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 6414 . 2 (𝑓 = 𝐹 → (𝑓 Fn 𝐴𝐹 Fn 𝐴))
2 elixp2 8450 . . 3 (𝑓X𝑥𝐴 𝐵 ↔ (𝑓 ∈ V ∧ 𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵))
32simp2bi 1143 . 2 (𝑓X𝑥𝐴 𝐵𝑓 Fn 𝐴)
41, 3vtoclga 3522 1 (𝐹X𝑥𝐴 𝐵𝐹 Fn 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 2111  ∀wral 3106  Vcvv 3441   Fn wfn 6319  ‘cfv 6324  Xcixp 8446 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-iota 6283  df-fun 6326  df-fn 6327  df-fv 6332  df-ixp 8447 This theorem is referenced by:  ixpprc  8468  undifixp  8483  resixpfo  8485  boxcutc  8490  ixpiunwdom  9040  prdsbasfn  16738  xpsff1o  16834  sscfn1  17081  funcfn2  17133  natfn  17218  pthaus  22250  ptuncnv  22419  ptunhmeo  22420  ptcmplem2  22665  prdsbl  23105  finixpnum  35058  upixp  35183  prdstotbnd  35248  elixpconstg  41740  rrxsnicc  42957  ioorrnopnxrlem  42963  hoidmvlelem3  43251  hspdifhsp  43270  hspmbllem2  43281
 Copyright terms: Public domain W3C validator