Theorem f1ocnvdm 7305

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 6861	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
2		f1of 6849	. . 3 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → ◡𝐹:𝐵⟶𝐴)
3	1, 2	syl 17	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵⟶𝐴)
4	3	ffvelcdmda 7104	1 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (◡𝐹‘𝐶) ∈ 𝐴)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2106  ^◡ccnv 5688  ⟶wf 6559  –1-1-onto→wf1o 6562  ‘cfv 6563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571

This theorem is referenced by:  f1oiso2  7372  f1ocnvfv3  7426  dif1enlem  9195  dif1enlemOLD  9196  rexdif1en  9197  rexdif1enOLD  9198  dif1en  9199  dif1enOLD  9201  uzrdglem  13995  uzrdgsuci  13998  fzennn  14006  cardfz  14008  fzfi  14010  iunmbl2  25606  noseqrdglem  28326  noseqrdgsuc  28329  f1otrg  28894  axcontlem10  29003  wlkiswwlks2lem5  29903  clwlkclwwlklem2a  30027  cnvbraval  32139  cnvbracl  32140  cycpmco2lem6  33134  cycpmco2  33136  mndpluscn  33887  ismtycnv  37789  rngoisocnv  37968  lautcnvclN  40071  lautcnvle  40072  lautcvr  40075  lautj  40076  lautm  40077  ltrncnvatb  40121  diacnvclN  41034  dihcnvcl  41254  dihlspsnat  41316  dihglblem6  41323  dochocss  41349  dochnoncon  41374  mapdcnvcl  41635  rmxyelxp  42901  cantnfub  43311  isuspgrim0lem  47809  isuspgrim0  47810  uspgrimprop  47811  uhgrimisgrgriclem  47836  clnbgrgrimlem  47839  uspgrlimlem3  47893  grlicsym  47909