![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fniniseg | Structured version Visualization version GIF version |
Description: Membership in the preimage of a singleton, under a function. (Contributed by Mario Carneiro, 12-May-2014.) (Proof shortened by Mario Carneiro , 28-Apr-2015.) |
Ref | Expression |
---|---|
fniniseg | ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elpreima 6652 | . 2 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵}))) | |
2 | fvex 6510 | . . . 4 ⊢ (𝐹‘𝐶) ∈ V | |
3 | 2 | elsn 4451 | . . 3 ⊢ ((𝐹‘𝐶) ∈ {𝐵} ↔ (𝐹‘𝐶) = 𝐵) |
4 | 3 | anbi2i 614 | . 2 ⊢ ((𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵)) |
5 | 1, 4 | syl6bb 279 | 1 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 387 = wceq 1508 ∈ wcel 2051 {csn 4436 ◡ccnv 5403 “ cima 5407 Fn wfn 6181 ‘cfv 6186 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-13 2302 ax-ext 2745 ax-sep 5057 ax-nul 5064 ax-pr 5183 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-3an 1071 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-mo 2548 df-eu 2585 df-clab 2754 df-cleq 2766 df-clel 2841 df-nfc 2913 df-ne 2963 df-ral 3088 df-rex 3089 df-rab 3092 df-v 3412 df-sbc 3677 df-dif 3827 df-un 3829 df-in 3831 df-ss 3838 df-nul 4174 df-if 4346 df-sn 4437 df-pr 4439 df-op 4443 df-uni 4710 df-br 4927 df-opab 4989 df-id 5309 df-xp 5410 df-rel 5411 df-cnv 5412 df-co 5413 df-dm 5414 df-rn 5415 df-res 5416 df-ima 5417 df-iota 6150 df-fun 6188 df-fn 6189 df-fv 6194 |
This theorem is referenced by: fparlem1 7614 fparlem2 7615 pw2f1olem 8416 recmulnq 10183 dmrecnq 10187 vdwlem1 16172 vdwlem2 16173 vdwlem6 16177 vdwlem8 16179 vdwlem9 16180 vdwlem12 16183 vdwlem13 16184 ramval 16199 ramub1lem1 16217 ghmeqker 18169 efgrelexlemb 18649 efgredeu 18651 psgnevpmb 20449 qtopeu 22044 itg1addlem1 24012 i1faddlem 24013 i1fmullem 24014 i1fmulclem 24022 i1fres 24025 itg10a 24030 itg1ge0a 24031 itg1climres 24034 mbfi1fseqlem4 24038 ply1remlem 24475 ply1rem 24476 fta1glem1 24478 fta1glem2 24479 fta1g 24480 fta1blem 24481 plyco0 24501 ofmulrt 24590 plyremlem 24612 plyrem 24613 fta1lem 24615 fta1 24616 vieta1lem1 24618 vieta1lem2 24619 vieta1 24620 plyexmo 24621 elaa 24624 aannenlem1 24636 aalioulem2 24641 pilem1 24758 efif1olem3 24845 efif1olem4 24846 efifo 24848 eff1olem 24849 basellem4 25379 lgsqrlem2 25641 lgsqrlem3 25642 rpvmasum2 25806 dirith 25823 foresf1o 30060 ofpreima 30190 fnpreimac 30196 1stpreimas 30218 s3clhash 30391 dimkerim 30685 locfinreflem 30781 qqhre 30938 indpi1 30956 indpreima 30961 sibfof 31276 cvmliftlem6 32155 cvmliftlem7 32156 cvmliftlem8 32157 cvmliftlem9 32158 taupilem3 34075 itg2addnclem 34417 itg2addnclem2 34418 pw2f1o2val2 39067 dnnumch3 39077 proot1mul 39229 proot1hash 39230 proot1ex 39231 wessf1ornlem 40900 |
Copyright terms: Public domain | W3C validator |