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

Theorem fnmpti 5921
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 5918 . 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 4638   Fn wfn 5785
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 4704  ax-nul 4712  ax-pr 4828
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-rex 2902  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 4579  df-opab 4639  df-mpt 4640  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-fun 5792  df-fn 5793
This theorem is referenced by:  dmmpti  5922  fconst  5989  dffn5  6136  eufnfv  6373  idref  6381  offn  6784  caofinvl  6800  fo1st  7057  fo2nd  7058  reldm  7088  mapsnf1o2  7769  unfilem2  8088  fidomdm  8106  pwfilem  8121  noinfep  8418  aceq3lem  8804  dfac4  8806  ackbij2lem2  8923  cfslb2n  8951  axcc2lem  9119  konigthlem  9247  rankcf  9456  tskuni  9462  seqf1o  12662  ccatlen  13162  ccatvalfn  13167  swrdlen  13224  swrdswrd  13261  sqrtf  13900  mptfzshft  14301  fsumrev  14302  fprodrev  14495  efcvgfsum  14604  prmreclem2  15408  1arith  15418  vdwlem6  15477  vdwlem8  15479  slotfn  15658  topnfn  15858  fnmre  16023  cidffn  16111  cidfn  16112  funcres  16328  yonedainv  16693  fn0g  17034  grpinvfn  17234  conjnmz  17466  psgnfn  17693  odf  17728  sylow1lem4  17788  pgpssslw  17801  sylow2blem3  17809  sylow3lem2  17815  cygctb  18065  dprd2da  18213  fnmgp  18263  rlmfn  18960  rrgsupp  19061  asclfn  19106  evlslem1  19285  frlmup4  19907  mdetrlin  20175  fncld  20584  hauseqlcld  21207  kqf  21308  filunirn  21444  fmf  21507  txflf  21568  clsnsg  21671  tgpconcomp  21674  qustgpopn  21681  qustgplem  21682  ustfn  21763  xmetunirn  21900  met1stc  22084  rrxmvallem  22940  ovolf  23002  vitali  23133  i1fmulc  23221  mbfi1fseqlem4  23236  itg2seq  23260  itg2monolem1  23268  i1fibl  23325  fncpn  23447  lhop1lem  23525  mdegxrf  23577  aannenlem3  23834  efabl  24045  logccv  24154  gausslemma2dlem1  24836  padicabvf  25065  mptelee  25521  wlkiswwlk2lem1  26013  clwlkisclwwlklem2a2  26102  grpoinvf  26564  occllem  27340  pjfni  27738  pjmfn  27752  rnbra  28144  bra11  28145  kbass2  28154  hmopidmchi  28188  xppreima2  28624  abfmpunirn  28626  dmct  28671  psgnfzto1stlem  28975  fimaproj  29022  locfinreflem  29029  ofcfn  29283  sxbrsigalem3  29455  eulerpartgbij  29555  sseqfv1  29572  sseqfn  29573  sseqf  29575  sseqfv2  29577  signstlen  29764  msubrn  30474  msrf  30487  faclimlem1  30676  matunitlindflem1  32369  poimirlem30  32403  mblfinlem2  32411  volsupnfl  32418  cnambfre  32422  itg2addnclem2  32426  itg2addnclem3  32427  ftc1anclem5  32453  ftc1anclem7  32455  sdclem2  32502  prdsbnd2  32558  rrncmslem  32595  diafn  35135  cdlemm10N  35219  dibfna  35255  lcfrlem9  35651  mapd1o  35749  hdmapfnN  35933  hgmapfnN  35992  rmxypairf1o  36288  hbtlem6  36512  dgraaf  36530  cytpfn  36599  ntrf  37235  uzmptshftfval  37361  binomcxplemrat  37365  addrfn  37491  subrfn  37492  mulvfn  37493  fourierdlem62  38855  fourierdlem70  38863  fourierdlem71  38864  fmtnorn  39779  1wlkiswwlks2lem1  41058  clwlkclwwlklem2a2  41194  zrinitorngc  41784  zrtermorngc  41785  zrtermoringc  41854
  Copyright terms: Public domain W3C validator