Theorem f1ocnvdm 7279

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ^◡ccnv 5674  ⟶wf 6536  –1-1-onto→wf1o 6539  ‘cfv 6540

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548

This theorem is referenced by:  f1oiso2  7345  f1ocnvfv3  7400  dif1enlem  9152  dif1enlemOLD  9153  rexdif1en  9154  rexdif1enOLD  9155  dif1en  9156  dif1enOLD  9158  uzrdglem  13918  uzrdgsuci  13921  fzennn  13929  cardfz  13931  fzfi  13933  iunmbl2  25065  f1otrg  28111  axcontlem10  28220  wlkiswwlks2lem5  29116  clwlkclwwlklem2a  29240  cnvbraval  31350  cnvbracl  31351  cycpmco2lem6  32277  cycpmco2  32279  mndpluscn  32894  ismtycnv  36658  rngoisocnv  36837  lautcnvclN  38947  lautcnvle  38948  lautcvr  38951  lautj  38952  lautm  38953  ltrncnvatb  38997  diacnvclN  39910  dihcnvcl  40130  dihlspsnat  40192  dihglblem6  40199  dochocss  40225  dochnoncon  40250  mapdcnvcl  40511  rmxyelxp  41636  cantnfub  42056  isomuspgrlem1  46481  isomgrsym  46490