Theorem f1ocnvdm 7236

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 6801	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
2		f1of 6789	. . 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 396   ∈ wcel 2106  ^◡ccnv 5637  ⟶wf 6497  –1-1-onto→wf1o 6500  ‘cfv 6501

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 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389

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 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509

This theorem is referenced by:  f1oiso2  7302  f1ocnvfv3  7357  dif1enlem  9107  dif1enlemOLD  9108  rexdif1en  9109  rexdif1enOLD  9110  dif1en  9111  dif1enOLD  9113  uzrdglem  13872  uzrdgsuci  13875  fzennn  13883  cardfz  13885  fzfi  13887  iunmbl2  24958  f1otrg  27876  axcontlem10  27985  wlkiswwlks2lem5  28881  clwlkclwwlklem2a  29005  cnvbraval  31115  cnvbracl  31116  cycpmco2lem6  32050  cycpmco2  32052  mndpluscn  32596  ismtycnv  36334  rngoisocnv  36513  lautcnvclN  38624  lautcnvle  38625  lautcvr  38628  lautj  38629  lautm  38630  ltrncnvatb  38674  diacnvclN  39587  dihcnvcl  39807  dihlspsnat  39869  dihglblem6  39876  dochocss  39902  dochnoncon  39927  mapdcnvcl  40188  rmxyelxp  41294  cantnfub  41714  isomuspgrlem1  46139  isomgrsym  46148