Theorem funfn 5622

Description: An equivalence for the function predicate. (Contributed by NM, 13-Aug-2004.)

Assertion

Ref	Expression
funfn

Proof of Theorem funfn

Step	Hyp	Ref	Expression
1		eqid 2457	. . 3
2	1	biantru 505	. 2
3		df-fn 5596	. 2
4	2, 3	bitr4i 252	1

Syntax hints:  <->wb 184  /\wa 369  =wceq 1395  domcdm 5004  Funwfun 5587  Fnwfn 5588

This theorem is referenced by:  funssxp  5749  funforn  5807  funbrfvb  5915  funopfvb  5916  ssimaex  5938  fvco  5949  fvco4i  5951  eqfunfv  5986  fvimacnvi  6001  unpreima  6013  respreima  6016  elrnrexdm  6035  elrnrexdmb  6036  ffvresb  6062  funressn  6084  funresdfunsn  6113  resfunexg  6137  funex  6140  funiunfv  6160  elunirn  6163  suppval1  6924  funsssuppss  6945  smores  7042  smores2  7044  tfrlem1  7064  rdgsucg  7108  rdglimg  7110  mptfi  7839  resfifsupp  7877  ordtypelem4  7967  ordtypelem6  7969  ordtypelem7  7970  ordtypelem9  7972  ordtypelem10  7973  harwdom  8037  ackbij2  8644  brdom3  8927  brdom5  8928  brdom4  8929  smobeth  8982  fpwwe2lem11  9039  hashkf  12407  hashfun  12495  hashimarn  12496  fclim  13376  isstruct2  14641  xpsc0  14957  xpsc1  14958  invf  15162  coapm  15398  psgnghm  18616  lindfrn  18856  ofco2  18953  dfac14  20119  perfdvf  22307  c1lip2  22399  taylf  22756  usgra2edg  24382  usgrarnedg  24384  usgrafilem2  24412  cusgrares  24472  vdusgraval  24907  vdgrnn0pnf  24909  vdn0frgrav2  25023  vdgn0frgrav2  25024  vdgfrgragt2  25027  hlimf  26155  adj1o  26813  abrexdomjm  27405  iunpreima  27432  unipreima  27484  xppreima  27487  mptct  27541  mptctf  27544  sitgf  28289  orvcval2  28397  wfrlem4  29346  frrlem4  29390  elno3  29415  fullfunfnv  29596  fullfunfv  29597  abrexdom  30221  funcoressn  32212  funbrafvb  32241  funopafvb  32242  resfnfinfin  32310  fundmfibi  32311  residfi  32314  uhgraopsiz  32392  diaf11N  36776  dibf11N  36888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2449  df-fn 5596