Theorem fniniseg 5987

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.)

Assertion

Ref	Expression
fniniseg	|- ( F Fn A -> ( C e. ( `' F " { B } ) <-> ( C e. A /\ ( F ` C ) = B ) ) )

Proof of Theorem fniniseg

Step	Hyp	Ref	Expression
1		elpreima 5986	. 2 |- ( F Fn A -> ( C e. ( `' F " { B } ) <-> ( C e. A /\ ( F ` C ) e. { B } ) ) )
2		fvex 5858	. . . 4 |- ( F ` C ) e. _V
3	2	elsnc 3960	. . 3 |- ( ( F ` C ) e. { B } <-> ( F ` C ) = B )
4	3	anbi2i 705	. 2 |- ( ( C e. A /\ ( F ` C ) e. { B } ) <-> ( C e. A /\ ( F ` C ) = B ) )
5	1, 4	syl6bb 269	1 |- ( F Fn A -> ( C e. ( `' F " { B } ) <-> ( C e. A /\ ( F ` C ) = B ) ) )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375   = wceq 1448   e. wcel 1891   {csn 3936   `'ccnv 4811   "cima 4815   Fn wfn 5556   ` cfv 5561

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