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

Theorem fnmpti 6202
Description: Functionality and domain of an ordered-pair class abstraction. (Contributed by NM, 29-Jan-2004.) (Revised by Mario Carneiro, 31-Aug-2015.)
Hypotheses
Ref Expression
fnmpti.1 𝐵 ∈ V
fnmpti.2 𝐹 = (𝑥𝐴𝐵)
Assertion
Ref Expression
fnmpti 𝐹 Fn 𝐴
Distinct variable group:   𝑥,𝐴
Allowed substitution hints:   𝐵(𝑥)   𝐹(𝑥)

Proof of Theorem fnmpti
StepHypRef Expression
1 fnmpti.1 . . 3 𝐵 ∈ V
21rgenw 3071 . 2 𝑥𝐴 𝐵 ∈ V
3 fnmpti.2 . . 3 𝐹 = (𝑥𝐴𝐵)
43mptfng 6199 . 2 (∀𝑥𝐴 𝐵 ∈ V ↔ 𝐹 Fn 𝐴)
52, 4mpbi 221 1 𝐹 Fn 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1652  wcel 2155  wral 3055  Vcvv 3350  cmpt 4890   Fn wfn 6065
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4943  ax-nul 4951  ax-pr 5064
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ral 3060  df-rab 3064  df-v 3352  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-nul 4082  df-if 4246  df-sn 4337  df-pr 4339  df-op 4343  df-br 4812  df-opab 4874  df-mpt 4891  df-id 5187  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-fun 6072  df-fn 6073
This theorem is referenced by:  dmmpti  6203  fconst  6275  dffn5  6432  idref  6605  eufnfv  6686  offn  7108  caofinvl  7124  fo1st  7388  fo2nd  7389  reldm  7421  mapsnf1o2  8112  unfilem2  8434  fidomdm  8452  pwfilem  8469  noinfep  8774  aceq3lem  9196  dfac4  9198  ackbij2lem2  9317  cfslb2n  9345  axcc2lem  9513  dmct  9601  konigthlem  9645  rankcf  9854  tskuni  9860  seqf1o  13052  ccatlen  13549  ccatvalfn  13555  swrdlen  13627  swrdswrd  13695  sqrtf  14391  mptfzshft  14797  fprodrev  14993  efcvgfsum  15101  prmreclem2  15903  1arith  15913  vdwlem6  15972  vdwlem8  15974  slotfn  16151  topnfn  16355  fnmre  16520  cidffn  16607  cidfn  16608  funcres  16824  yonedainv  17190  fn0g  17531  grpinvfn  17732  conjnmz  17961  psgnfn  18188  odf  18223  sylow1lem4  18283  pgpssslw  18296  sylow2blem3  18304  sylow3lem2  18310  cygctb  18562  dprd2da  18711  fnmgp  18761  rlmfn  19467  rrgsupp  19568  asclfn  19613  evlslem1  19791  frlmup4  20419  mdetrlin  20688  fncld  21109  hauseqlcld  21732  kqf  21833  filunirn  21968  fmf  22031  txflf  22092  clsnsg  22195  tgpconncomp  22198  qustgpopn  22205  qustgplem  22206  ustfn  22287  xmetunirn  22424  met1stc  22608  rrxmvallem  23479  ovolf  23543  vitali  23674  i1fmulc  23764  mbfi1fseqlem4  23779  itg2seq  23803  itg2monolem1  23811  i1fibl  23868  fncpn  23990  lhop1lem  24070  mdegxrf  24122  aannenlem3  24379  efabl  24591  logccv  24703  gausslemma2dlem1  25385  padicabvf  25614  mptelee  26069  wlkiswwlks2lem1  27063  clwlkclwwlklem2a2  27223  grpoinvf  27846  occllem  28621  pjfni  29019  pjmfn  29033  rnbra  29425  bra11  29426  kbass2  29435  hmopidmchi  29469  xppreima2  29903  abfmpunirn  29905  psgnfzto1stlem  30300  fimaproj  30350  locfinreflem  30357  ofcfn  30612  sxbrsigalem3  30784  eulerpartgbij  30884  sseqfv1  30902  sseqfn  30903  sseqf  30905  sseqfv2  30907  signstlen  31096  msubrn  31877  msrf  31890  faclimlem1  32077  bj-evalfn  33457  matunitlindflem1  33832  poimirlem30  33866  mblfinlem2  33874  volsupnfl  33881  cnambfre  33884  itg2addnclem2  33888  itg2addnclem3  33889  ftc1anclem5  33915  ftc1anclem7  33917  sdclem2  33963  prdsbnd2  34019  rrncmslem  34056  diafn  36993  cdlemm10N  37077  dibfna  37113  lcfrlem9  37509  mapd1o  37607  hdmapfnN  37788  hgmapfnN  37847  rmxypairf1o  38156  hbtlem6  38379  dgraaf  38397  cytpfn  38466  ntrf  39098  uzmptshftfval  39222  binomcxplemrat  39226  addrfn  39351  subrfn  39352  mulvfn  39353  limsup10exlem  40645  liminfvalxr  40656  fourierdlem62  41025  fourierdlem70  41033  fourierdlem71  41034  fmtnorn  42125  zrinitorngc  42672  zrtermorngc  42673  zrtermoringc  42742
  Copyright terms: Public domain W3C validator