![]() |
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 6480 | . 2 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵}))) | |
2 | fvex 6342 | . . . 4 ⊢ (𝐹‘𝐶) ∈ V | |
3 | 2 | elsn 4329 | . . 3 ⊢ ((𝐹‘𝐶) ∈ {𝐵} ↔ (𝐹‘𝐶) = 𝐵) |
4 | 3 | anbi2i 601 | . 2 ⊢ ((𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵)) |
5 | 1, 4 | syl6bb 276 | 1 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 382 = wceq 1630 ∈ wcel 2144 {csn 4314 ◡ccnv 5248 “ cima 5252 Fn wfn 6026 ‘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-ne 2943 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-res 5261 df-ima 5262 df-iota 5994 df-fun 6033 df-fn 6034 df-fv 6039 |
This theorem is referenced by: fparlem1 7427 fparlem2 7428 pw2f1olem 8219 recmulnq 9987 dmrecnq 9991 vdwlem1 15891 vdwlem2 15892 vdwlem6 15896 vdwlem8 15898 vdwlem9 15899 vdwlem12 15902 vdwlem13 15903 ramval 15918 ramub1lem1 15936 ghmeqker 17894 efgrelexlemb 18369 efgredeu 18371 psgnevpmb 20147 qtopeu 21739 itg1addlem1 23678 i1faddlem 23679 i1fmullem 23680 i1fmulclem 23688 i1fres 23691 itg10a 23696 itg1ge0a 23697 itg1climres 23700 mbfi1fseqlem4 23704 ply1remlem 24141 ply1rem 24142 fta1glem1 24144 fta1glem2 24145 fta1g 24146 fta1blem 24147 plyco0 24167 ofmulrt 24256 plyremlem 24278 plyrem 24279 fta1lem 24281 fta1 24282 vieta1lem1 24284 vieta1lem2 24285 vieta1 24286 plyexmo 24287 elaa 24290 aannenlem1 24302 aalioulem2 24307 pilem1 24424 efif1olem3 24510 efif1olem4 24511 efifo 24513 eff1olem 24514 basellem4 25030 lgsqrlem2 25292 lgsqrlem3 25293 rpvmasum2 25421 dirith 25438 foresf1o 29675 ofpreima 29799 1stpreimas 29817 locfinreflem 30241 qqhre 30398 indpi1 30416 indpreima 30421 sibfof 30736 cvmliftlem6 31604 cvmliftlem7 31605 cvmliftlem8 31606 cvmliftlem9 31607 taupilem3 33495 itg2addnclem 33786 itg2addnclem2 33787 pw2f1o2val2 38126 dnnumch3 38136 proot1mul 38296 proot1hash 38297 proot1ex 38298 wessf1ornlem 39885 |
Copyright terms: Public domain | W3C validator |