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

Theorem fnmpti 5935
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 2908 . 2 𝑥𝐴 𝐵 ∈ V
3 fnmpti.2 . . 3 𝐹 = (𝑥𝐴𝐵)
43mptfng 5932 . 2 (∀𝑥𝐴 𝐵 ∈ V ↔ 𝐹 Fn 𝐴)
52, 4mpbi 219 1 𝐹 Fn 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1475  wcel 1977  wral 2896  Vcvv 3173  cmpt 4643   Fn wfn 5799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-fun 5806  df-fn 5807
This theorem is referenced by:  dmmpti  5936  fconst  6004  dffn5  6151  eufnfv  6395  idref  6403  offn  6806  caofinvl  6822  fo1st  7079  fo2nd  7080  reldm  7110  mapsnf1o2  7791  unfilem2  8110  fidomdm  8128  pwfilem  8143  noinfep  8440  aceq3lem  8826  dfac4  8828  ackbij2lem2  8945  cfslb2n  8973  axcc2lem  9141  konigthlem  9269  rankcf  9478  tskuni  9484  seqf1o  12704  ccatlen  13213  ccatvalfn  13218  swrdlen  13275  swrdswrd  13312  sqrtf  13951  mptfzshft  14352  fsumrev  14353  fprodrev  14546  efcvgfsum  14655  prmreclem2  15459  1arith  15469  vdwlem6  15528  vdwlem8  15530  slotfn  15709  topnfn  15909  fnmre  16074  cidffn  16162  cidfn  16163  funcres  16379  yonedainv  16744  fn0g  17085  grpinvfn  17285  conjnmz  17517  psgnfn  17744  odf  17779  sylow1lem4  17839  pgpssslw  17852  sylow2blem3  17860  sylow3lem2  17866  cygctb  18116  dprd2da  18264  fnmgp  18314  rlmfn  19011  rrgsupp  19112  asclfn  19157  evlslem1  19336  frlmup4  19959  mdetrlin  20227  fncld  20636  hauseqlcld  21259  kqf  21360  filunirn  21496  fmf  21559  txflf  21620  clsnsg  21723  tgpconcomp  21726  qustgpopn  21733  qustgplem  21734  ustfn  21815  xmetunirn  21952  met1stc  22136  rrxmvallem  22995  ovolf  23057  vitali  23188  i1fmulc  23276  mbfi1fseqlem4  23291  itg2seq  23315  itg2monolem1  23323  i1fibl  23380  fncpn  23502  lhop1lem  23580  mdegxrf  23632  aannenlem3  23889  efabl  24100  logccv  24209  gausslemma2dlem1  24891  padicabvf  25120  mptelee  25575  wlkiswwlk2lem1  26219  clwlkisclwwlklem2a2  26308  grpoinvf  26770  occllem  27546  pjfni  27944  pjmfn  27958  rnbra  28350  bra11  28351  kbass2  28360  hmopidmchi  28394  xppreima2  28830  abfmpunirn  28832  dmct  28877  psgnfzto1stlem  29181  fimaproj  29228  locfinreflem  29235  ofcfn  29489  sxbrsigalem3  29661  eulerpartgbij  29761  sseqfv1  29778  sseqfn  29779  sseqf  29781  sseqfv2  29783  signstlen  29970  msubrn  30680  msrf  30693  faclimlem1  30882  matunitlindflem1  32575  poimirlem30  32609  mblfinlem2  32617  volsupnfl  32624  cnambfre  32628  itg2addnclem2  32632  itg2addnclem3  32633  ftc1anclem5  32659  ftc1anclem7  32661  sdclem2  32708  prdsbnd2  32764  rrncmslem  32801  diafn  35341  cdlemm10N  35425  dibfna  35461  lcfrlem9  35857  mapd1o  35955  hdmapfnN  36139  hgmapfnN  36198  rmxypairf1o  36494  hbtlem6  36718  dgraaf  36736  cytpfn  36805  ntrf  37441  uzmptshftfval  37567  binomcxplemrat  37571  addrfn  37697  subrfn  37698  mulvfn  37699  fourierdlem62  39061  fourierdlem70  39069  fourierdlem71  39070  fmtnorn  39984  1wlkiswwlks2lem1  41066  clwlkclwwlklem2a2  41202  zrinitorngc  41792  zrtermorngc  41793  zrtermoringc  41862
  Copyright terms: Public domain W3C validator