Theorem f1ocnvdm 7293

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144  ^◡ccnv 5649  ⟶wf 6534  –1-1-onto→wf1o 6537  ‘cfv 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546

This theorem is used by:  f1oiso2  7360  f1ocnvfv3  7415  dif1enlem  9175  rexdif1en  9176  dif1en  9177  uzrdglem  14100  uzrdgsuci  14103  fzennn  14111  cardfz  14113  fzfi  14115  iunmbl2  25878  addonbday  28665  noseqrdglem  28691  noseqrdgsuc  28694  bdayfinlem  28872  f1otrg  29448  axcontlem10  29551  wlkiswwlks2lem5  30462  clwlkclwwlklem2a  30589  cnvbraval  32712  cnvbracl  32713  cycpmco2lem6  33692  cycpmco2  33694  mndpluscn  34558  vonf1oonfo  35898  ismtycnv  38737  rngoisocnv  38916  lautcnvclN  41146  lautcnvle  41147  lautcvr  41150  lautj  41151  lautm  41152  ltrncnvatb  41196  diacnvclN  42109  dihcnvcl  42329  dihlspsnat  42391  dihglblem6  42398  dochocss  42424  dochnoncon  42449  mapdcnvcl  42710  rmxyelxp  43919  cantnfub  44323  isuspgrim0lem  48991  isuspgrim0  48992  upgrimwlklem2  48996  upgrimtrls  49004  uhgrimisgrgriclem  49028  clnbgrgrimlem  49031  uspgrlimlem3  49088  grlicsym  49111  imaf1homlem  50215  uptrar  50324