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

Theorem funcnvcnv 6620
Description: The double converse of a function is a function. (Contributed by NM, 21-Sep-2004.)
Assertion
Ref Expression
funcnvcnv (Fun 𝐴 → Fun 𝐴)

Proof of Theorem funcnvcnv
StepHypRef Expression
1 cnvcnvss 6198 . 2 𝐴𝐴
2 funss 6572 . 2 (𝐴𝐴 → (Fun 𝐴 → Fun 𝐴))
31, 2ax-mp 5 1 (Fun 𝐴 → Fun 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3947  ccnv 5677  Fun wfun 6542
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-sep 5299  ax-nul 5306  ax-pr 5429
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3430  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5149  df-opab 5211  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-fun 6550
This theorem is referenced by:  funcnvres2  6633  inpreima  7073  difpreima  7074  f1oresrab  7136  sbthlem8  9114  fin1a2lem7  10429  cnclima  23171  iscncl  23172  qtopcld  23616  qtoprest  23620  qtopcmap  23622  rnelfmlem  23855  fmfnfmlem3  23859  mbfimaicc  25559  ismbf3d  25582  i1fd  25609  gsummpt2co  32762
  Copyright terms: Public domain W3C validator