MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  f1ocnvdm Structured version   Visualization version   GIF version

Theorem f1ocnvdm 6682
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
StepHypRef Expression
1 f1ocnv 6290 . . 3 (𝐹:𝐴1-1-onto𝐵𝐹:𝐵1-1-onto𝐴)
2 f1of 6278 . . 3 (𝐹:𝐵1-1-onto𝐴𝐹:𝐵𝐴)
31, 2syl 17 . 2 (𝐹:𝐴1-1-onto𝐵𝐹:𝐵𝐴)
43ffvelrnda 6502 1 ((𝐹:𝐴1-1-onto𝐵𝐶𝐵) → (𝐹𝐶) ∈ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 2144  ccnv 5248  wf 6027  1-1-ontowf1o 6030  cfv 6031
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-sep 4912  ax-nul 4920  ax-pr 5034
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-mo 2622  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ral 3065  df-rex 3066  df-rab 3069  df-v 3351  df-sbc 3586  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-nul 4062  df-if 4224  df-sn 4315  df-pr 4317  df-op 4321  df-uni 4573  df-br 4785  df-opab 4845  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039
This theorem is referenced by:  f1oiso2  6744  f1ocnvfv3  6788  uzrdglem  12963  uzrdgsuci  12966  fzennn  12974  cardfz  12976  fzfi  12978  iunmbl2  23544  f1otrg  25971  axcontlem10  26073  wlkiswwlks2lem5  27006  clwlkclwwlklem2a  27145  cnvbraval  29303  cnvbracl  29304  mndpluscn  30306  ismtycnv  33926  rngoisocnv  34105  lautcnvclN  35889  lautcnvle  35890  lautcvr  35893  lautj  35894  lautm  35895  ltrncnvatb  35939  diacnvclN  36854  dihcnvcl  37074  dihlspsnat  37136  dihglblem6  37143  dochocss  37169  dochnoncon  37194  mapdcnvcl  37455  rmxyelxp  37996
  Copyright terms: Public domain W3C validator