Theorem f1ocnvdm 7026

Description: The value of the converse of a one-to-one onto function belongs to its domain. (Contributed by NM, 26-May-2006.)

Assertion

Ref	Expression
f1ocnvdm	⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (◡𝐹‘𝐶) ∈ 𝐴)

Proof of Theorem f1ocnvdm

Step	Hyp	Ref	Expression
1		f1ocnv 6607	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
2		f1of 6595	. . 3 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → ◡𝐹:𝐵⟶𝐴)
3	1, 2	syl 17	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵⟶𝐴)
4	3	ffvelrnda 6835	1 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (◡𝐹‘𝐶) ∈ 𝐴)

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2112  ^◡ccnv 5516  ⟶wf 6324  –1-1-onto→wf1o 6327  ‘cfv 6328

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5162  ax-nul 5169  ax-pr 5291

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3an 1087  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2899  df-ral 3073  df-rex 3074  df-v 3409  df-sbc 3694  df-dif 3857  df-un 3859  df-in 3861  df-ss 3871  df-nul 4222  df-if 4414  df-sn 4516  df-pr 4518  df-op 4522  df-uni 4792  df-br 5026  df-opab 5088  df-id 5423  df-xp 5523  df-rel 5524  df-cnv 5525  df-co 5526  df-dm 5527  df-rn 5528  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336

This theorem is referenced by:  f1oiso2  7092  f1ocnvfv3  7139  dif1enlem  8765  rexdif1en  8766  dif1en  8767  uzrdglem  13359  uzrdgsuci  13362  fzennn  13370  cardfz  13372  fzfi  13374  iunmbl2  24242  f1otrg  26749  axcontlem10  26851  wlkiswwlks2lem5  27743  clwlkclwwlklem2a  27867  cnvbraval  29977  cnvbracl  29978  cycpmco2lem6  30909  cycpmco2  30911  mndpluscn  31382  ismtycnv  35505  rngoisocnv  35684  lautcnvclN  37649  lautcnvle  37650  lautcvr  37653  lautj  37654  lautm  37655  ltrncnvatb  37699  diacnvclN  38612  dihcnvcl  38832  dihlspsnat  38894  dihglblem6  38901  dochocss  38927  dochnoncon  38952  mapdcnvcl  39213  rmxyelxp  40211  isomuspgrlem1  44697  isomgrsym  44706