Theorem f1imacnv 5674

Description: Preimage of an image. (Contributed by NM, 30-Sep-2004.)

Assertion

Ref	Expression
f1imacnv

Proof of Theorem f1imacnv

Step	Hyp	Ref	Expression
1		resima 5165	. 2
2		df-f1 5443	. . . . . . 7
3	2	simprbi 452	. . . . . 6
4	3	adantr 453	. . . . 5
5		funcnvres 5505	. . . . 5
6	4, 5	syl 16	. . . 4
7	6	imaeq1d 5191	. . 3
8		f1ores 5672	. . . . 5
9		f1ocnv 5670	. . . . 5
10	8, 9	syl 16	. . . 4
11		imadmrn 5202	. . . . 5
12		f1odm 5662	. . . . . 6
13	12	imaeq2d 5192	. . . . 5
14		f1ofo 5665	. . . . . 6
15		forn 5640	. . . . . 6
16	14, 15	syl 16	. . . . 5
17	11, 13, 16	3eqtr3a 2545	. . . 4
18	10, 17	syl 16	. . 3
19	7, 18	eqtr3d 2523	. 2
20	1, 19	syl5eqr 2535	1

Syntax hints:  ->wi 4  /\wa 360  =wceq 1670  C_wss 3365  `'ccnv 4861  domcdm 4862  rancrn 4863  |`cres 4864  "cima 4865  Funwfun 5432  -->wf 5434  -1-1->wf1 5435  -onto->wfo 5436  -1-1-onto->wf1o 5437

This theorem is referenced by:  f1opw2  6323  ssenen  7446  f1opwfi  7577  isf34lem3  8426  subggim  15624  gicsubgen  15636  cnt1  18428  basqtop  18758  tgqtop  18759  hmeoopn  18813  hmeocld  18814  hmeontr  18816  qtopf1  18863  tpr2rico  25521  eulerpartlemmf  25932  ballotlemscr  26051  ballotlemrinv0  26065  cvmlift2lem9a  26338  grpokerinj  27932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-9 1736  ax-10 1751  ax-11 1756  ax-12 1768  ax-13 1955  ax-ext 2470  ax-sep 4439  ax-nul 4447  ax-pr 4554

This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1338  df-ex 1566  df-nf 1569  df-sb 1677  df-eu 2317  df-mo 2318  df-clab 2476  df-cleq 2482  df-clel 2485  df-nfc 2614  df-ne 2654  df-ral 2764  df-rex 2765  df-rab 2768  df-v 3017  df-dif 3368  df-un 3370  df-in 3372  df-ss 3379  df-nul 3674  df-if 3826  df-sn 3915  df-pr 3916  df-op 3918  df-br 4319  df-opab 4377  df-id 4657  df-xp 4868  df-rel 4869  df-cnv 4870  df-co 4871  df-dm 4872  df-rn 4873  df-res 4874  df-ima 4875  df-fun 5440  df-fn 5441  df-f 5442  df-f1 5443  df-fo 5444  df-f1o 5445