Theorem fnmpti 5714

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
fnmpti.2

Assertion

Ref	Expression
fnmpti

Distinct variable group:   ,

Proof of Theorem fnmpti

Step	Hyp	Ref	Expression
1		fnmpti.1	. . 3
2	1	rgenw 2818	. 2
3		fnmpti.2	. . 3
4	3	mptfng 5711	. 2
5	2, 4	mpbi 208	1

Syntax hints:  =wceq 1395  e.wcel 1818  A.wral 2807  cvv 3109  e.cmpt 4510  Fnwfn 5588

This theorem is referenced by:  dmmpti  5715  fconst  5776  dffn5  5918  eufnfv  6146  idref  6153  offn  6551  caofinvl  6567  fo1st  6820  fo2nd  6821  reldm  6851  mapsnf1o2  7486  unfilem2  7805  fidomdm  7822  pwfilem  7834  noinfep  8097  aceq3lem  8522  dfac4  8524  ackbij2lem2  8641  cfslb2n  8669  axcc2lem  8837  konigthlem  8964  rankcf  9176  tskuni  9182  seqf1o  12148  ccatlen  12594  ccatvalfn  12599  swrdlen  12650  swrdvalfn  12663  swrdswrd  12685  sqrtf  13196  mptfzshft  13593  fsumrev  13594  fprodrev  13781  efcvgfsum  13821  prmreclem2  14435  1arith  14445  vdwlem6  14504  vdwlem8  14506  slotfn  14646  topnfn  14823  fnmre  14988  cidffn  15075  cidfn  15076  funcres  15265  yonedainv  15550  fn0g  15889  grpinvfn  16090  conjnmz  16300  psgnfn  16526  odf  16561  sylow1lem4  16621  pgpssslw  16634  sylow2blem3  16642  sylow3lem2  16648  cygctb  16894  dprd2da  17091  fnmgp  17143  rlmfn  17836  rrgsupp  17939  asclfn  17985  evlslem1  18184  frlmup4  18835  mdetrlin  19104  fncld  19523  hauseqlcld  20147  kqf  20248  filunirn  20383  fmf  20446  txflf  20507  clsnsg  20608  tgpconcomp  20611  qustgpopn  20618  qustgplem  20619  ustfn  20704  xmetunirn  20840  met1stc  21024  rrxmvallem  21831  ovolf  21893  vitali  22022  i1fmulc  22110  mbfi1fseqlem4  22125  itg2seq  22149  itg2monolem1  22157  i1fibl  22214  fncpn  22336  lhop1lem  22414  mdegxrf  22468  aannenlem3  22726  efabl  22937  logccv  23044  padicabvf  23816  mptelee  24198  wlkiswwlk2lem1  24691  clwlkisclwwlklem2a2  24780  fngid  25216  grpoinvf  25242  occllem  26221  pjfni  26619  pjmfn  26633  rnbra  27026  bra11  27027  kbass2  27036  hmopidmchi  27070  xppreima2  27488  abfmpunirn  27490  dmct  27537  fimaproj  27836  locfinreflem  27843  ofcfn  28099  sxbrsigalem3  28243  eulerpartgbij  28311  sseqfv1  28328  sseqfn  28329  sseqf  28331  sseqfv2  28333  signstlen  28524  msubrn  28889  msrf  28902  faclimlem1  29168  mblfinlem2  30052  volsupnfl  30059  cnambfre  30063  itg2addnclem2  30067  itg2addnclem3  30068  ftc1anclem5  30094  ftc1anclem7  30096  sdclem2  30235  prdsbnd2  30291  rrncmslem  30328  rmxypairf1o  30847  hbtlem6  31078  dgraaf  31096  cytpfn  31168  uzmptshftfval  31251  binomcxplemrat  31255  addrfn  31381  subrfn  31382  mulvfn  31383  fourierdlem62  31951  fourierdlem70  31959  fourierdlem71  31960  zrinitorngc  32808  zrtermorngc  32809  zrtermoringc  32878  diafn  36761  cdlemm10N  36845  dibfna  36881  lcfrlem9  37277  mapd1o  37375  hdmapfnN  37559  hgmapfnN  37618

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-fun 5595  df-fn 5596