Theorem f1ocnvdm 7231

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ^◡ccnv 5623  ⟶wf 6488  –1-1-onto→wf1o 6491  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500

This theorem is referenced by:  f1oiso2  7298  f1ocnvfv3  7353  dif1enlem  9084  rexdif1en  9085  dif1en  9086  uzrdglem  13880  uzrdgsuci  13883  fzennn  13891  cardfz  13893  fzfi  13895  iunmbl2  25514  addonbday  28275  noseqrdglem  28301  noseqrdgsuc  28304  bdayfinlem  28482  f1otrg  28943  axcontlem10  29046  wlkiswwlks2lem5  29946  clwlkclwwlklem2a  30073  cnvbraval  32185  cnvbracl  32186  cycpmco2lem6  33213  cycpmco2  33215  mndpluscn  34083  ismtycnv  37999  rngoisocnv  38178  lautcnvclN  40344  lautcnvle  40345  lautcvr  40348  lautj  40349  lautm  40350  ltrncnvatb  40394  diacnvclN  41307  dihcnvcl  41527  dihlspsnat  41589  dihglblem6  41596  dochocss  41622  dochnoncon  41647  mapdcnvcl  41908  rmxyelxp  43150  cantnfub  43559  isuspgrim0lem  48135  isuspgrim0  48136  upgrimwlklem2  48140  upgrimtrls  48148  uhgrimisgrgriclem  48172  clnbgrgrimlem  48175  uspgrlimlem3  48232  grlicsym  48255  imaf1homlem  49348  uptrar  49457