Theorem funcnvcnv 6407

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

Step	Hyp	Ref	Expression
1		cnvcnvss 6037	. 2 ⊢ ◡◡𝐴 ⊆ 𝐴
2		funss 6360	. 2 ⊢ (◡◡𝐴 ⊆ 𝐴 → (Fun 𝐴 → Fun ◡◡𝐴))
3	1, 2	ax-mp 5	1 ⊢ (Fun 𝐴 → Fun ◡◡𝐴)

Syntax hints:   → wi 4   ⊆ wss 3924  ^◡ccnv 5540  Fun wfun 6335

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5189  ax-nul 5196  ax-pr 5316

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3488  df-dif 3927  df-un 3929  df-in 3931  df-ss 3940  df-nul 4280  df-if 4454  df-sn 4554  df-pr 4556  df-op 4560  df-br 5053  df-opab 5115  df-xp 5547  df-rel 5548  df-cnv 5549  df-co 5550  df-fun 6343

This theorem is referenced by:  funcnvres2  6420  inpreima  6820  difpreima  6821  f1oresrab  6875  sbthlem8  8620  fin1a2lem7  9814  cnclima  21859  iscncl  21860  qtopcld  22304  qtoprest  22308  qtopcmap  22310  rnelfmlem  22543  fmfnfmlem3  22547  mbfimaicc  24215  ismbf3d  24238  i1fd  24265  gsummpt2co  30693