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

Theorem f1ocnvfv 6000
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 5706 . . 3  |-  ( D  =  ( F `  C )  ->  ( `' F `  D )  =  ( `' F `  ( F `  C
) ) )
21eqcoms 2446 . 2  |-  ( ( F `  C )  =  D  ->  ( `' F `  D )  =  ( `' F `  ( F `  C
) ) )
3 f1ocnvfv1 5998 . . 3  |-  ( ( F : A -1-1-onto-> B  /\  C  e.  A )  ->  ( `' F `  ( F `  C ) )  =  C )
43eqeq2d 2454 . 2  |-  ( ( F : A -1-1-onto-> B  /\  C  e.  A )  ->  ( ( `' F `  D )  =  ( `' F `  ( F `
 C ) )  <-> 
( `' F `  D )  =  C ) )
52, 4syl5ib 219 1  |-  ( ( F : A -1-1-onto-> B  /\  C  e.  A )  ->  ( ( F `  C )  =  D  ->  ( `' F `  D )  =  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1369    e. wcel 1756   `'ccnv 4854   -1-1-onto->wf1o 5432   ` cfv 5433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4428  ax-nul 4436  ax-pow 4485  ax-pr 4546
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2735  df-rex 2736  df-rab 2739  df-v 2989  df-sbc 3202  df-dif 3346  df-un 3348  df-in 3350  df-ss 3357  df-nul 3653  df-if 3807  df-sn 3893  df-pr 3895  df-op 3899  df-uni 4107  df-br 4308  df-opab 4366  df-id 4651  df-xp 4861  df-rel 4862  df-cnv 4863  df-co 4864  df-dm 4865  df-rn 4866  df-res 4867  df-ima 4868  df-iota 5396  df-fun 5435  df-fn 5436  df-f 5437  df-f1 5438  df-fo 5439  df-f1o 5440  df-fv 5441
This theorem is referenced by:  f1ocnvfvb  6001  f1oiso2  6058  curry1  6679  curry2  6682  mapfienlem2  7670  infxpenc2lem1  8200  axcclem  8641  uzrdgfni  11796  uzrdgsuci  11798  fzennn  11805  axdc4uzlem  11819  seqf1olem1  11860  seqf1olem2  11861  hashginv  12122  sadaddlem  13677  xpsaddlem  14528  xpsvsca  14532  xpsle  14534  catcisolem  14989  mhmf1o  15488  ghmf1o  15791  lmhmf1o  17142  symgtgp  19687  xpsdsval  19971  cnvbraval  25529  derangenlem  27074  subfacp1lem4  27086  subfacp1lem5  27087  cvmliftlem9  27197  rngoisocnv  28806  cdleme51finvfvN  34218  ltrniotacnvval  34245
  Copyright terms: Public domain W3C validator