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

Theorem fnmpti 6487
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 3154 . 2 𝑥𝐴 𝐵 ∈ V
3 fnmpti.2 . . 3 𝐹 = (𝑥𝐴𝐵)
43mptfng 6483 . 2 (∀𝑥𝐴 𝐵 ∈ V ↔ 𝐹 Fn 𝐴)
52, 4mpbi 231 1 𝐹 Fn 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530  wcel 2107  wral 3142  Vcvv 3499  cmpt 5142   Fn wfn 6346
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797  ax-sep 5199  ax-nul 5206  ax-pr 5325
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ral 3147  df-rab 3151  df-v 3501  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4470  df-sn 4564  df-pr 4566  df-op 4570  df-br 5063  df-opab 5125  df-mpt 5143  df-id 5458  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-fun 6353  df-fn 6354
This theorem is referenced by:  dmmpti  6488  fconst  6561  dffn5  6720  idref  6903  eufnfv  6989  offn  7413  caofinvl  7429  fo1st  7703  fo2nd  7704  reldm  7737  fimaproj  7823  mapsnf1o2  8450  unfilem2  8775  fidomdm  8793  pwfilem  8810  noinfep  9115  aceq3lem  9538  dfac4  9540  ackbij2lem2  9654  cfslb2n  9682  axcc2lem  9850  dmct  9938  konigthlem  9982  rankcf  10191  tskuni  10197  seqf1o  13404  ccatlen  13920  ccatlenOLD  13921  ccatvalfn  13928  swrdlen  14002  swrdwrdsymb  14017  swrdswrd  14060  sqrtf  14716  mptfzshft  15126  fprodrev  15324  efcvgfsum  15432  prmreclem2  16246  1arith  16256  vdwlem6  16315  vdwlem8  16317  slotfn  16494  topnfn  16692  fnmre  16855  cidffn  16942  cidfn  16943  funcres  17159  yonedainv  17524  fn0g  17865  grpinvfn  18078  cycsubmel  18276  conjnmz  18325  psgnfn  18552  odf  18588  sylow1lem4  18649  pgpssslw  18662  sylow2blem3  18670  sylow3lem2  18676  cygctb  18935  dprd2da  19087  fnmgp  19164  rlmfn  19885  rrgsupp  19986  asclfn  20032  evlslem1  20216  frlmup4  20864  mdetrlin  21130  fncld  21549  hauseqlcld  22173  kqf  22274  filunirn  22409  fmf  22472  txflf  22533  clsnsg  22636  tgpconncomp  22639  qustgpopn  22646  qustgplem  22647  ustfn  22728  xmetunirn  22865  met1stc  23049  rrxmvallem  23925  ovolf  24001  vitali  24132  i1fmulc  24222  mbfi1fseqlem4  24237  itg2seq  24261  itg2monolem1  24269  i1fibl  24326  fncpn  24448  lhop1lem  24528  mdegxrf  24580  aannenlem3  24837  efabl  25050  logccv  25162  gausslemma2dlem1  25859  padicabvf  26124  mptelee  26598  wlkiswwlks2lem1  27564  clwlkclwwlklem2a2  27688  grpoinvf  28226  occllem  28997  pjfni  29395  pjmfn  29409  rnbra  29801  bra11  29802  kbass2  29811  hmopidmchi  29845  xppreima2  30313  abfmpunirn  30315  psgnfzto1stlem  30659  locfinreflem  30993  ofcfn  31248  sxbrsigalem3  31419  eulerpartgbij  31519  sseqfv1  31536  sseqfn  31537  sseqf  31539  sseqfv2  31541  signstlen  31726  msubrn  32663  msrf  32676  faclimlem1  32862  bj-evalfn  34249  bj-inftyexpitaufo  34366  matunitlindflem1  34758  poimirlem30  34792  mblfinlem2  34800  volsupnfl  34807  cnambfre  34810  itg2addnclem2  34814  itg2addnclem3  34815  ftc1anclem5  34841  ftc1anclem7  34843  sdclem2  34888  prdsbnd2  34944  rrncmslem  34981  diafn  38040  cdlemm10N  38124  dibfna  38160  lcfrlem9  38556  mapd1o  38654  hdmapfnN  38835  hgmapfnN  38894  rmxypairf1o  39376  hbtlem6  39597  dgraaf  39615  cytpfn  39676  ntrf  40341  uzmptshftfval  40546  binomcxplemrat  40550  addrfn  40672  subrfn  40673  mulvfn  40674  limsup10exlem  41921  liminfvalxr  41932  fourierdlem62  42322  fourierdlem70  42330  fourierdlem71  42331  fmtnorn  43531  zrinitorngc  44106  zrtermorngc  44107  zrtermoringc  44176
  Copyright terms: Public domain W3C validator