MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  f1imacnv Unicode version

Theorem f1imacnv 5651
Description: Preimage of an image. (Contributed by NM, 30-Sep-2004.)
Assertion
Ref Expression
f1imacnv

Proof of Theorem f1imacnv
StepHypRef Expression
1 resima 5147 . 2
2 df-f1 5422 . . . . . . 7
32simprbi 452 . . . . . 6
43adantr 453 . . . . 5
5 funcnvres 5484 . . . . 5
64, 5syl 16 . . . 4
76imaeq1d 5170 . . 3
8 f1ores 5649 . . . . 5
9 f1ocnv 5647 . . . . 5
108, 9syl 16 . . . 4
11 imadmrn 5181 . . . . 5
12 f1odm 5639 . . . . . 6
1312imaeq2d 5171 . . . . 5
14 f1ofo 5642 . . . . . 6
15 forn 5617 . . . . . 6
1614, 15syl 16 . . . . 5
1711, 13, 163eqtr3a 2537 . . . 4
1810, 17syl 16 . . 3
197, 18eqtr3d 2515 . 2
201, 19syl5eqr 2527 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  /\wa 360  =wceq 1662  C_wss 3353  `'ccnv 4843  domcdm 4844  rancrn 4845  |`cres 4846  "cima 4847  Funwfun 5411  -->wf 5413  -1-1->wf1 5414  -onto->wfo 5415  -1-1-onto->wf1o 5416
This theorem is referenced by:  f1opw2  6280  ssenen  7393  f1opwfi  7522  isf34lem3  8369  subggim  15556  gicsubgen  15568  cnt1  17917  basqtop  18247  tgqtop  18248  hmeoopn  18302  hmeocld  18303  hmeontr  18305  qtopf1  18352  tpr2rico  25012  eulerpartlemmf  25423  ballotlemscr  25542  ballotlemrinv0  25556  cvmlift2lem9a  25829  grpokerinj  27423
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1562  ax-4 1573  ax-5 1636  ax-6 1677  ax-7 1697  ax-9 1728  ax-10 1743  ax-11 1748  ax-12 1760  ax-13 1947  ax-ext 2462  ax-sep 4423  ax-nul 4431  ax-pr 4538
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1337  df-ex 1558  df-nf 1561  df-sb 1669  df-eu 2309  df-mo 2310  df-clab 2468  df-cleq 2474  df-clel 2477  df-nfc 2606  df-ne 2646  df-ral 2756  df-rex 2757  df-rab 2760  df-v 3008  df-dif 3356  df-un 3358  df-in 3360  df-ss 3367  df-nul 3661  df-if 3813  df-sn 3900  df-pr 3901  df-op 3903  df-br 4303  df-opab 4361  df-id 4639  df-xp 4850  df-rel 4851  df-cnv 4852  df-co 4853  df-dm 4854  df-rn 4855  df-res 4856  df-ima 4857  df-fun 5419  df-fn 5420  df-f 5421  df-f1 5422  df-fo 5423  df-f1o 5424
  Copyright terms: Public domain W3C validator