Theorem f1ocnvdm 7039

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111  ^◡ccnv 5527  ⟶wf 6336  –1-1-onto→wf1o 6339  ‘cfv 6340

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5173  ax-nul 5180  ax-pr 5302

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ral 3075  df-rex 3076  df-v 3411  df-sbc 3699  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5037  df-opab 5099  df-id 5434  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-iota 6299  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348

This theorem is referenced by:  f1oiso2  7105  f1ocnvfv3  7152  dif1enlem  8744  rexdif1en  8745  dif1en  8746  uzrdglem  13387  uzrdgsuci  13390  fzennn  13398  cardfz  13400  fzfi  13402  iunmbl2  24271  f1otrg  26778  axcontlem10  26880  wlkiswwlks2lem5  27772  clwlkclwwlklem2a  27896  cnvbraval  30006  cnvbracl  30007  cycpmco2lem6  30937  cycpmco2  30939  mndpluscn  31410  ismtycnv  35555  rngoisocnv  35734  lautcnvclN  37699  lautcnvle  37700  lautcvr  37703  lautj  37704  lautm  37705  ltrncnvatb  37749  diacnvclN  38662  dihcnvcl  38882  dihlspsnat  38944  dihglblem6  38951  dochocss  38977  dochnoncon  39002  mapdcnvcl  39263  rmxyelxp  40271  isomuspgrlem1  44771  isomgrsym  44780