Theorem dff13 6166

Description: A one-to-one function in terms of function values. Compare Theorem 4.8(iv) of [Monk1] p. 43. (Contributed by NM, 29-Oct-1996.)

Assertion

Ref	Expression
dff13

Distinct variable groups:   ,,   ,,

Proof of Theorem dff13

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dff12 5785	. 2
2		ffn 5736	. . . 4
3		vex 3112	. . . . . . . . . . . . . . 15
4		vex 3112	. . . . . . . . . . . . . . 15
5	3, 4	breldm 5212	. . . . . . . . . . . . . 14
6		fndm 5685	. . . . . . . . . . . . . . 15
7	6	eleq2d 2527	. . . . . . . . . . . . . 14
8	5, 7	syl5ib 219	. . . . . . . . . . . . 13
9		vex 3112	. . . . . . . . . . . . . . 15
10	9, 4	breldm 5212	. . . . . . . . . . . . . 14
11	6	eleq2d 2527	. . . . . . . . . . . . . 14
12	10, 11	syl5ib 219	. . . . . . . . . . . . 13
13	8, 12	anim12d 563	. . . . . . . . . . . 12
14	13	pm4.71rd 635	. . . . . . . . . . 11
15		eqcom 2466	. . . . . . . . . . . . . . 15
16		fnbrfvb 5913	. . . . . . . . . . . . . . 15
17	15, 16	syl5bb 257	. . . . . . . . . . . . . 14
18		eqcom 2466	. . . . . . . . . . . . . . 15
19		fnbrfvb 5913	. . . . . . . . . . . . . . 15
20	18, 19	syl5bb 257	. . . . . . . . . . . . . 14
21	17, 20	bi2anan9 873	. . . . . . . . . . . . 13
22	21	anandis 830	. . . . . . . . . . . 12
23	22	pm5.32da 641	. . . . . . . . . . 11
24	14, 23	bitr4d 256	. . . . . . . . . 10
25	24	imbi1d 317	. . . . . . . . 9
26		impexp 446	. . . . . . . . 9
27	25, 26	syl6bb 261	. . . . . . . 8
28	27	albidv 1713	. . . . . . 7
29		19.21v 1729	. . . . . . . 8
30		19.23v 1760	. . . . . . . . . 10
31		fvex 5881	. . . . . . . . . . . 12
32	31	eqvinc 3226	. . . . . . . . . . 11
33	32	imbi1i 325	. . . . . . . . . 10
34	30, 33	bitr4i 252	. . . . . . . . 9
35	34	imbi2i 312	. . . . . . . 8
36	29, 35	bitri 249	. . . . . . 7
37	28, 36	syl6bb 261	. . . . . 6
38	37	2albidv 1715	. . . . 5
39		breq1 4455	. . . . . . . 8
40	39	mo4 2337	. . . . . . 7
41	40	albii 1640	. . . . . 6
42		alrot3 1846	. . . . . 6
43	41, 42	bitri 249	. . . . 5
44		r2al 2835	. . . . 5
45	38, 43, 44	3bitr4g 288	. . . 4
46	2, 45	syl 16	. . 3
47	46	pm5.32i 637	. 2
48	1, 47	bitri 249	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369  A.wal 1393  =wceq 1395  E.wex 1612  e.wcel 1818  E*wmo 2283  A.wral 2807   class class class wbr 4452  domcdm 5004  Fnwfn 5588  -->wf 5589  -1-1->wf1 5590  `cfv 5593

This theorem is referenced by:  dff13f  6167  f1veqaeq  6168  dff14a  6177  dff1o6  6181  fcof1  6190  soisoi  6224  f1o2ndf1  6908  fnwelem  6915  smo11  7054  tz7.48lem  7125  omsmo  7322  unxpdomlem3  7746  unfilem2  7805  fofinf1o  7821  inf3lem6  8071  r111  8214  fseqenlem1  8426  fodomacn  8458  alephf1  8487  alephiso  8500  ackbij1lem17  8637  infpssrlem5  8708  fin23lem28  8741  fin1a2lem2  8802  fin1a2lem4  8804  axcc2lem  8837  domtriomlem  8843  cnref1o  11244  injresinj  11926  om2uzf1oi  12064  wwlktovf1  12895  reeff1  13855  bitsf1  14096  crt  14308  eulerthlem2  14312  1arith  14445  vdwlem12  14510  xpsff1o  14965  setcmon  15414  yoniso  15554  ghmf1  16295  orbsta  16351  symgextf1  16446  symgfixf1  16462  odf1  16584  kerf1hrm  17392  mvrf1  18081  ply1sclf1  18330  znf1o  18590  cygznlem3  18608  uvcf1  18823  lindff1  18855  scmatf1  19033  mdetunilem8  19121  mat2pmatf1  19230  pm2mpf1  19300  ist0-4  20230  ovolicc2lem4  21931  recosf1o  22922  efif1olem4  22932  basellem4  23357  dvdsmulf1o  23470  lgsqrlem2  23617  lgseisenlem2  23625  axlowdimlem15  24259  wlkntrllem3  24563  wlkdvspthlem  24609  fargshiftf1  24637  constr3trllem2  24651  wlknwwlkninj  24711  wlkiswwlkinj  24718  wwlkextinj  24730  clwwlkf1  24796  clwlkf1clwwlk  24850  frgrancvvdeqlemB  25038  numclwlk1lem2f1  25094  pjmf1  26634  unopf1o  26835  erdszelem9  28643  mrsubff1  28874  msubff1  28916  mvhf1  28919  ghomf1olem  29034  f1opr  30215  grpokerinj  30347  dnnumch3  30993  sumnnodd  31636  dvnprodlem1  31743  fourierdlem34  31923  fourierdlem51  31940  fthestrcsetc  32656  embedsetcestrclem  32663  fthsetcestrc  32671  cdleme50f1  36269  dihf11  36994

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-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fv 5601