Theorem funcnvcnv 6605

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 6186	. 2 ⊢ ◡◡𝐴 ⊆ 𝐴
2		funss 6556	. 2 ⊢ (◡◡𝐴 ⊆ 𝐴 → (Fun 𝐴 → Fun ◡◡𝐴))
3	1, 2	ax-mp 5	1 ⊢ (Fun 𝐴 → Fun ◡◡𝐴)

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3899  ^◡ccnv 5650  Fun wfun 6531

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-res 5663  df-fun 6539

This theorem is used by:  funcnvres2  6618  inpreima  7061  difpreima  7062  f1oresrab  7126  sbthlem8  9106  fin1a2lem7  10477  cnclima  23579  iscncl  23580  qtopcld  24025  qtoprest  24029  qtopcmap  24031  rnelfmlem  24264  fmfnfmlem3  24268  mbfimaicc  25945  ismbf3d  25968  i1fd  25995  gsummpt2co  33602