Theorem f1ocnvdm 7243

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ^◡ccnv 5633  ⟶wf 6498  –1-1-onto→wf1o 6501  ‘cfv 6502

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-12 2185  ax-ext 2709  ax-sep 5245  ax-nul 5255  ax-pr 5381

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-id 5529  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510

This theorem is referenced by:  f1oiso2  7310  f1ocnvfv3  7365  dif1enlem  9098  rexdif1en  9099  dif1en  9100  uzrdglem  13894  uzrdgsuci  13897  fzennn  13905  cardfz  13907  fzfi  13909  iunmbl2  25531  addonbday  28292  noseqrdglem  28318  noseqrdgsuc  28321  bdayfinlem  28499  f1otrg  28961  axcontlem10  29064  wlkiswwlks2lem5  29964  clwlkclwwlklem2a  30091  cnvbraval  32204  cnvbracl  32205  cycpmco2lem6  33231  cycpmco2  33233  mndpluscn  34110  ismtycnv  38082  rngoisocnv  38261  lautcnvclN  40493  lautcnvle  40494  lautcvr  40497  lautj  40498  lautm  40499  ltrncnvatb  40543  diacnvclN  41456  dihcnvcl  41676  dihlspsnat  41738  dihglblem6  41745  dochocss  41771  dochnoncon  41796  mapdcnvcl  42057  rmxyelxp  43298  cantnfub  43707  isuspgrim0lem  48282  isuspgrim0  48283  upgrimwlklem2  48287  upgrimtrls  48295  uhgrimisgrgriclem  48319  clnbgrgrimlem  48322  uspgrlimlem3  48379  grlicsym  48402  imaf1homlem  49495  uptrar  49604