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

Theorem funcnvcnv 5627
Description: The double converse of a function is a function. (Contributed by NM, 21-Sep-2004.)
Assertion
Ref Expression
funcnvcnv  |-  ( Fun 
A  ->  Fun  `' `' A )

Proof of Theorem funcnvcnv
StepHypRef Expression
1 cnvcnvss 5278 . 2  |-  `' `' A  C_  A
2 funss 5587 . 2  |-  ( `' `' A  C_  A  -> 
( Fun  A  ->  Fun  `' `' A ) )
31, 2ax-mp 5 1  |-  ( Fun 
A  ->  Fun  `' `' A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3414   `'ccnv 4822   Fun wfun 5563
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4517  ax-nul 4525  ax-pr 4630
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2759  df-rex 2760  df-rab 2763  df-v 3061  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-nul 3739  df-if 3886  df-sn 3973  df-pr 3975  df-op 3979  df-br 4396  df-opab 4454  df-xp 4829  df-rel 4830  df-cnv 4831  df-co 4832  df-fun 5571
This theorem is referenced by:  funcnvres2  5640  inpreima  5992  difpreima  5993  f1oresrab  6042  sbthlem8  7672  mapfienOLD  8170  fin1a2lem7  8818  strlemor0  14935  cnclima  20062  iscncl  20063  qtopcld  20506  qtoprest  20510  qtopcmap  20512  rnelfmlem  20745  fmfnfmlem3  20749  mbfimaicc  22332  ismbf3d  22353  i1fd  22380  gsummpt2co  28222
  Copyright terms: Public domain W3C validator