![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fniniseg | Structured version Visualization version Unicode 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 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elpreima 5986 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | fvex 5858 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | elsnc 3960 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | anbi2i 705 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | syl6bb 269 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1673 ax-4 1686 ax-5 1762 ax-6 1809 ax-7 1855 ax-9 1900 ax-10 1919 ax-11 1924 ax-12 1937 ax-13 2092 ax-ext 2432 ax-sep 4497 ax-nul 4506 ax-pr 4612 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 988 df-tru 1451 df-ex 1668 df-nf 1672 df-sb 1802 df-eu 2304 df-mo 2305 df-clab 2439 df-cleq 2445 df-clel 2448 df-nfc 2582 df-ne 2624 df-ral 2742 df-rex 2743 df-rab 2746 df-v 3015 df-sbc 3236 df-dif 3375 df-un 3377 df-in 3379 df-ss 3386 df-nul 3700 df-if 3850 df-sn 3937 df-pr 3939 df-op 3943 df-uni 4169 df-br 4375 df-opab 4434 df-id 4727 df-xp 4818 df-rel 4819 df-cnv 4820 df-co 4821 df-dm 4822 df-rn 4823 df-res 4824 df-ima 4825 df-iota 5525 df-fun 5563 df-fn 5564 df-fv 5569 |
This theorem is referenced by: fparlem1 6884 fparlem2 6885 pw2f1olem 7663 recmulnq 9376 dmrecnq 9380 vdwlem1 14942 vdwlem2 14943 vdwlem6 14947 vdwlem8 14949 vdwlem9 14950 vdwlem12 14953 vdwlem13 14954 ramval 14971 ramvalOLD 14972 ramub1lem1 14995 ghmeqker 16920 efgrelexlemb 17411 efgredeu 17413 psgnevpmb 19166 qtopeu 20742 itg1addlem1 22662 i1faddlem 22663 i1fmullem 22664 i1fmulclem 22672 i1fres 22675 itg10a 22680 itg1ge0a 22681 itg1climres 22684 mbfi1fseqlem4 22688 ply1remlem 23125 ply1rem 23126 fta1glem1 23128 fta1glem2 23129 fta1g 23130 fta1blem 23131 plyco0 23158 ofmulrt 23247 plyremlem 23269 plyrem 23270 fta1lem 23272 fta1 23273 vieta1lem1 23275 vieta1lem2 23276 vieta1 23277 plyexmo 23278 elaa 23281 aannenlem1 23296 aalioulem2 23301 pilem1 23418 efif1olem3 23505 efif1olem4 23506 efifo 23508 eff1olem 23509 basellem4 24022 lgsqrlem2 24282 lgsqrlem3 24283 rpvmasum2 24362 dirith 24379 foresf1o 28151 ofpreima 28276 1stpreimas 28294 locfinreflem 28674 qqhre 28831 indpi1 28850 indpreima 28853 sibfof 29179 cvmliftlem6 30019 cvmliftlem7 30020 cvmliftlem8 30021 cvmliftlem9 30022 taupilem3 31722 itg2addnclem 31995 itg2addnclem2 31996 pw2f1o2val2 35897 dnnumch3 35907 proot1mul 36075 proot1hash 36079 proot1ex 36080 wessf1ornlem 37469 |
Copyright terms: Public domain | W3C validator |