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 6785	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
2		f1of 6773	. . 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 2114  ^◡ccnv 5622  ⟶wf 6487  –1-1-onto→wf1o 6490  ‘cfv 6491

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 2183  ax-ext 2707  ax-sep 5240  ax-nul 5250  ax-pr 5376

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 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-ne 2932  df-ral 3051  df-rex 3060  df-rab 3399  df-v 3441  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4285  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-iota 6447  df-fun 6493  df-fn 6494  df-f 6495  df-f1 6496  df-fo 6497  df-f1o 6498  df-fv 6499

This theorem is referenced by:  f1oiso2  7298  f1ocnvfv3  7353  dif1enlem  9086  rexdif1en  9087  dif1en  9088  uzrdglem  13882  uzrdgsuci  13885  fzennn  13893  cardfz  13895  fzfi  13897  iunmbl2  25516  addsonbday  28258  noseqrdglem  28284  noseqrdgsuc  28287  bdayfinlem  28463  f1otrg  28924  axcontlem10  29027  wlkiswwlks2lem5  29927  clwlkclwwlklem2a  30054  cnvbraval  32166  cnvbracl  32167  cycpmco2lem6  33192  cycpmco2  33194  mndpluscn  34062  ismtycnv  37972  rngoisocnv  38151  lautcnvclN  40383  lautcnvle  40384  lautcvr  40387  lautj  40388  lautm  40389  ltrncnvatb  40433  diacnvclN  41346  dihcnvcl  41566  dihlspsnat  41628  dihglblem6  41635  dochocss  41661  dochnoncon  41686  mapdcnvcl  41947  rmxyelxp  43191  cantnfub  43600  isuspgrim0lem  48176  isuspgrim0  48177  upgrimwlklem2  48181  upgrimtrls  48189  uhgrimisgrgriclem  48213  clnbgrgrimlem  48216  uspgrlimlem3  48273  grlicsym  48296  imaf1homlem  49389  uptrar  49498