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

Theorem f1ocnvfv 5955
Description: Relationship between the value of a one-to-one onto function and the value of its converse. (Contributed by Raph Levien, 10-Apr-2004.)
Assertion
Ref Expression
f1ocnvfv  |-  ( ( F : A -1-1-onto-> B  /\  C  e.  A )  ->  ( ( F `  C )  =  D  ->  ( `' F `  D )  =  C ) )

Proof of Theorem f1ocnvfv
StepHypRef Expression
1 fveq2 5668 . . 3  |-  ( D  =  ( F `  C )  ->  ( `' F `  D )  =  ( `' F `  ( F `  C
) ) )
21eqcoms 2390 . 2  |-  ( ( F `  C )  =  D  ->  ( `' F `  D )  =  ( `' F `  ( F `  C
) ) )
3 f1ocnvfv1 5953 . . 3  |-  ( ( F : A -1-1-onto-> B  /\  C  e.  A )  ->  ( `' F `  ( F `  C ) )  =  C )
43eqeq2d 2398 . 2  |-  ( ( F : A -1-1-onto-> B  /\  C  e.  A )  ->  ( ( `' F `  D )  =  ( `' F `  ( F `
 C ) )  <-> 
( `' F `  D )  =  C ) )
52, 4syl5ib 211 1  |-  ( ( F : A -1-1-onto-> B  /\  C  e.  A )  ->  ( ( F `  C )  =  D  ->  ( `' F `  D )  =  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649    e. wcel 1717   `'ccnv 4817   -1-1-onto->wf1o 5393   ` cfv 5394
This theorem is referenced by:  f1ocnvfvb  5956  f1oiso2  6011  curry1  6377  curry2  6380  infxpenc2lem1  7833  axcclem  8270  uzrdgfni  11225  uzrdgsuci  11227  fzennn  11234  axdc4uzlem  11248  seqf1olem1  11289  seqf1olem2  11290  hashginv  11549  sadaddlem  12905  xpsaddlem  13727  xpsvsca  13731  xpsle  13733  catcisolem  14188  ghmf1o  14962  lmhmf1o  16049  symgtgp  18052  xpsdsval  18319  cnvbraval  23461  derangenlem  24636  subfacp1lem4  24648  subfacp1lem5  24649  cvmliftlem9  24759  rngoisocnv  26288  cdleme51finvfvN  30669  ltrniotacnvval  30696
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-sep 4271  ax-nul 4279  ax-pow 4318  ax-pr 4344
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2242  df-mo 2243  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-ral 2654  df-rex 2655  df-rab 2658  df-v 2901  df-sbc 3105  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-sn 3763  df-pr 3764  df-op 3766  df-uni 3958  df-br 4154  df-opab 4208  df-id 4439  df-xp 4824  df-rel 4825  df-cnv 4826  df-co 4827  df-dm 4828  df-rn 4829  df-res 4830  df-ima 4831  df-iota 5358  df-fun 5396  df-fn 5397  df-f 5398  df-f1 5399  df-fo 5400  df-f1o 5401  df-fv 5402
  Copyright terms: Public domain W3C validator