Theorem fniniseg 5812

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 5811	. 2 |- ( F Fn A -> ( C e. ( `' F " { B } ) <-> ( C e. A /\ ( F ` C ) e. { B } ) ) )
2		fvex 5689	. . . 4 |- ( F ` C ) e. _V
3	2	elsnc 3889	. . 3 |- ( ( F ` C ) e. { B } <-> ( F ` C ) = B )
4	3	anbi2i 687	. 2 |- ( ( C e. A /\ ( F ` C ) e. { B } ) <-> ( C e. A /\ ( F ` C ) = B ) )
5	1, 4	syl6bb 261	1 |- ( F Fn A -> ( C e. ( `' F " { B } ) <-> ( C e. A /\ ( F ` C ) = B ) ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1362   e. wcel 1755   {csn 3865   `'ccnv 4826   "cima 4830   Fn wfn 5401   ` cfv 5406

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pr 4519

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-id 4623  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-fv 5414

This theorem is referenced by:  fparlem1  6661  fparlem2  6662  pw2f1olem  7403  recmulnq  9121  dmrecnq  9125  vdwlem1  14025  vdwlem2  14026  vdwlem6  14030  vdwlem8  14032  vdwlem9  14033  vdwlem12  14036  vdwlem13  14037  ramval  14052  ramub1lem1  14070  ghmeqker  15753  efgrelexlemb  16227  efgredeu  16229  psgnevpmb  17859  qtopeu  19131  itg1addlem1  21012  i1faddlem  21013  i1fmullem  21014  i1fmulclem  21022  i1fres  21025  itg10a  21030  itg1ge0a  21031  itg1climres  21034  mbfi1fseqlem4  21038  ply1remlem  21519  ply1rem  21520  fta1glem1  21522  fta1glem2  21523  fta1g  21524  fta1blem  21525  plyco0  21545  ofmulrt  21633  plyremlem  21655  plyrem  21656  fta1lem  21658  fta1  21659  vieta1lem1  21661  vieta1lem2  21662  vieta1  21663  plyexmo  21664  elaa  21667  aannenlem1  21679  aalioulem2  21684  pilem1  21801  efif1olem3  21885  efif1olem4  21886  efifo  21888  eff1olem  21889  basellem4  22306  lgsqrlem2  22566  lgsqrlem3  22567  rpvmasum2  22646  dirith  22663  ofpreima  25808  qqhre  26300  indpi1  26332  indpreima  26335  sibfof  26574  cvmliftlem6  27027  cvmliftlem7  27028  cvmliftlem8  27029  cvmliftlem9  27030  itg2addnclem  28287  itg2addnclem2  28288  pw2f1o2val2  29234  dnnumch3  29245  proot1mul  29409  proot1hash  29413  proot1ex  29414  taupilem3  35185