| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > f1ocnvdm | Structured version Visualization version GIF version | ||
| Description: The value of the converse of a one-to-one onto function belongs to its domain. (Contributed by NM, 26-May-2006.) |
| Ref | Expression |
|---|---|
| f1ocnvdm | ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (◡𝐹‘𝐶) ∈ 𝐴) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | f1ocnv 6860 | . . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴) | |
| 2 | f1of 6848 | . . 3 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → ◡𝐹:𝐵⟶𝐴) | |
| 3 | 1, 2 | syl 17 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵⟶𝐴) |
| 4 | 3 | ffvelcdmda 7104 | 1 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (◡𝐹‘𝐶) ∈ 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2108 ◡ccnv 5684 ⟶wf 6557 –1-1-onto→wf1o 6560 ‘cfv 6561 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-opab 5206 df-id 5578 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 |
| This theorem is referenced by: f1oiso2 7372 f1ocnvfv3 7426 dif1enlem 9196 dif1enlemOLD 9197 rexdif1en 9198 rexdif1enOLD 9199 dif1en 9200 dif1enOLD 9202 uzrdglem 13998 uzrdgsuci 14001 fzennn 14009 cardfz 14011 fzfi 14013 iunmbl2 25592 noseqrdglem 28311 noseqrdgsuc 28314 f1otrg 28879 axcontlem10 28988 wlkiswwlks2lem5 29893 clwlkclwwlklem2a 30017 cnvbraval 32129 cnvbracl 32130 cycpmco2lem6 33151 cycpmco2 33153 mndpluscn 33925 ismtycnv 37809 rngoisocnv 37988 lautcnvclN 40090 lautcnvle 40091 lautcvr 40094 lautj 40095 lautm 40096 ltrncnvatb 40140 diacnvclN 41053 dihcnvcl 41273 dihlspsnat 41335 dihglblem6 41342 dochocss 41368 dochnoncon 41393 mapdcnvcl 41654 rmxyelxp 42924 cantnfub 43334 isuspgrim0lem 47871 isuspgrim0 47872 uspgrimprop 47873 uhgrimisgrgriclem 47898 clnbgrgrimlem 47901 uspgrlimlem3 47957 grlicsym 47973 |
| Copyright terms: Public domain | W3C validator |