Theorem funcnvcnv 6586

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

Syntax hints:   → wi 4   ⊆ wss 3917  ^◡ccnv 5640  Fun wfun 6508

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-fun 6516

This theorem is referenced by:  funcnvres2  6599  inpreima  7039  difpreima  7040  f1oresrab  7102  sbthlem8  9064  fin1a2lem7  10366  cnclima  23162  iscncl  23163  qtopcld  23607  qtoprest  23611  qtopcmap  23613  rnelfmlem  23846  fmfnfmlem3  23850  mbfimaicc  25539  ismbf3d  25562  i1fd  25589  gsummpt2co  32995