Theorem dffo3 6046

Description: An onto mapping expressed in terms of function values. (Contributed by NM, 29-Oct-2006.)

Assertion

Ref	Expression
dffo3

Distinct variable groups:   ,,   ,,   ,,

Proof of Theorem dffo3

Step	Hyp	Ref	Expression
1		dffo2 5804	. 2
2		ffn 5736	. . . . 5
3		fnrnfv 5919	. . . . . 6
4	3	eqeq1d 2459	. . . . 5
5	2, 4	syl 16	. . . 4
6		simpr 461	. . . . . . . . . . 11
7		ffvelrn 6029	. . . . . . . . . . . 12
8	7	adantr 465	. . . . . . . . . . 11
9	6, 8	eqeltrd 2545	. . . . . . . . . 10
10	9	exp31 604	. . . . . . . . 9
11	10	rexlimdv 2947	. . . . . . . 8
12	11	biantrurd 508	. . . . . . 7
13		dfbi2 628	. . . . . . 7
14	12, 13	syl6rbbr 264	. . . . . 6
15	14	albidv 1713	. . . . 5
16		abeq1 2582	. . . . 5
17		df-ral 2812	. . . . 5
18	15, 16, 17	3bitr4g 288	. . . 4
19	5, 18	bitrd 253	. . 3
20	19	pm5.32i 637	. 2
21	1, 20	bitri 249	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369  A.wal 1393  =wceq 1395  e.wcel 1818  {cab 2442  A.wral 2807  E.wrex 2808  rancrn 5005  Fnwfn 5588  -->wf 5589  -onto->wfo 5591  `cfv 5593

This theorem is referenced by:  dffo4  6047  foelrn  6050  foco2  6051  fcofo  6191  foov  6449  resixpfo  7527  fofinf1o  7821  wdom2d  8027  brwdom3  8029  isf32lem9  8762  hsmexlem2  8828  cnref1o  11244  wwlktovfo  12896  1arith  14445  orbsta  16351  symgextfo  16447  symgfixfo  16464  pwssplit1  17705  znf1o  18590  cygznlem3  18608  scmatfo  19032  m2cpmfo  19257  pm2mpfo  19315  recosf1o  22922  efif1olem4  22932  dvdsmulf1o  23470  wlknwwlknsur  24712  wlkiswwlksur  24719  wwlkextsur  24731  clwwlkfo  24797  clwlkfoclwwlk  24845  frgrancvvdeqlemC  25039  numclwlk1lem2fo  25095  subfacp1lem3  28626  cvmfolem  28724  finixpnum  30038  sumnnodd  31636  dvnprodlem1  31743  fourierdlem54  31943  fullestrcsetc  32657  fullsetcestrc  32672

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-sbc 3328  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-uni 4250  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-rn 5015  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-fo 5599  df-fv 5601