![]() |
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 6452 | . 2 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵}))) | |
2 | fvex 6314 | . . . 4 ⊢ (𝐹‘𝐶) ∈ V | |
3 | 2 | elsn 4300 | . . 3 ⊢ ((𝐹‘𝐶) ∈ {𝐵} ↔ (𝐹‘𝐶) = 𝐵) |
4 | 3 | anbi2i 732 | . 2 ⊢ ((𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵)) |
5 | 1, 4 | syl6bb 276 | 1 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 = wceq 1596 ∈ wcel 2103 {csn 4285 ◡ccnv 5217 “ cima 5221 Fn wfn 5996 ‘cfv 6001 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1835 ax-4 1850 ax-5 1952 ax-6 2018 ax-7 2054 ax-9 2112 ax-10 2132 ax-11 2147 ax-12 2160 ax-13 2355 ax-ext 2704 ax-sep 4889 ax-nul 4897 ax-pr 5011 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1599 df-ex 1818 df-nf 1823 df-sb 2011 df-eu 2575 df-mo 2576 df-clab 2711 df-cleq 2717 df-clel 2720 df-nfc 2855 df-ne 2897 df-ral 3019 df-rex 3020 df-rab 3023 df-v 3306 df-sbc 3542 df-dif 3683 df-un 3685 df-in 3687 df-ss 3694 df-nul 4024 df-if 4195 df-sn 4286 df-pr 4288 df-op 4292 df-uni 4545 df-br 4761 df-opab 4821 df-id 5128 df-xp 5224 df-rel 5225 df-cnv 5226 df-co 5227 df-dm 5228 df-rn 5229 df-res 5230 df-ima 5231 df-iota 5964 df-fun 6003 df-fn 6004 df-fv 6009 |
This theorem is referenced by: fparlem1 7397 fparlem2 7398 pw2f1olem 8180 recmulnq 9899 dmrecnq 9903 vdwlem1 15808 vdwlem2 15809 vdwlem6 15813 vdwlem8 15815 vdwlem9 15816 vdwlem12 15819 vdwlem13 15820 ramval 15835 ramub1lem1 15853 ghmeqker 17809 efgrelexlemb 18284 efgredeu 18286 psgnevpmb 20056 qtopeu 21642 itg1addlem1 23579 i1faddlem 23580 i1fmullem 23581 i1fmulclem 23589 i1fres 23592 itg10a 23597 itg1ge0a 23598 itg1climres 23601 mbfi1fseqlem4 23605 ply1remlem 24042 ply1rem 24043 fta1glem1 24045 fta1glem2 24046 fta1g 24047 fta1blem 24048 plyco0 24068 ofmulrt 24157 plyremlem 24179 plyrem 24180 fta1lem 24182 fta1 24183 vieta1lem1 24185 vieta1lem2 24186 vieta1 24187 plyexmo 24188 elaa 24191 aannenlem1 24203 aalioulem2 24208 pilem1 24325 efif1olem3 24410 efif1olem4 24411 efifo 24413 eff1olem 24414 basellem4 24930 lgsqrlem2 25192 lgsqrlem3 25193 rpvmasum2 25321 dirith 25338 foresf1o 29571 ofpreima 29695 1stpreimas 29713 locfinreflem 30137 qqhre 30294 indpi1 30312 indpreima 30317 sibfof 30632 cvmliftlem6 31500 cvmliftlem7 31501 cvmliftlem8 31502 cvmliftlem9 31503 taupilem3 33397 itg2addnclem 33693 itg2addnclem2 33694 pw2f1o2val2 38026 dnnumch3 38036 proot1mul 38196 proot1hash 38197 proot1ex 38198 wessf1ornlem 39787 |
Copyright terms: Public domain | W3C validator |