Theorem funcnvcnv 6607

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3906  ^◡ccnv 5662  Fun wfun 6534

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 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

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 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-res 5675  df-fun 6542

This theorem is used by:  funcnvres2  6620  inpreima  7063  difpreima  7064  f1oresrab  7127  sbthlem8  9089  fin1a2lem7  10405  cnclima  23475  iscncl  23476  qtopcld  23921  qtoprest  23925  qtopcmap  23927  rnelfmlem  24160  fmfnfmlem3  24164  mbfimaicc  25841  ismbf3d  25864  i1fd  25891  gsummpt2co  33432