Theorem fniniseg 5819

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 5818	. 2 |- ( F Fn A -> ( C e. ( `' F " { B } ) <-> ( C e. A /\ ( F ` C ) e. { B } ) ) )
2		fvex 5696	. . . 4 |- ( F ` C ) e. _V
3	2	elsnc 3896	. . 3 |- ( ( F ` C ) e. { B } <-> ( F ` C ) = B )
4	3	anbi2i 694	. 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 1369   e. wcel 1756   {csn 3872   `'ccnv 4834   "cima 4838   Fn wfn 5408   ` cfv 5413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pr 4526

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-sbc 3182  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-id 4631  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-fv 5421

This theorem is referenced by:  fparlem1  6667  fparlem2  6668  pw2f1olem  7407  recmulnq  9125  dmrecnq  9129  vdwlem1  14034  vdwlem2  14035  vdwlem6  14039  vdwlem8  14041  vdwlem9  14042  vdwlem12  14045  vdwlem13  14046  ramval  14061  ramub1lem1  14079  ghmeqker  15764  efgrelexlemb  16238  efgredeu  16240  psgnevpmb  17992  qtopeu  19264  itg1addlem1  21145  i1faddlem  21146  i1fmullem  21147  i1fmulclem  21155  i1fres  21158  itg10a  21163  itg1ge0a  21164  itg1climres  21167  mbfi1fseqlem4  21171  ply1remlem  21609  ply1rem  21610  fta1glem1  21612  fta1glem2  21613  fta1g  21614  fta1blem  21615  plyco0  21635  ofmulrt  21723  plyremlem  21745  plyrem  21746  fta1lem  21748  fta1  21749  vieta1lem1  21751  vieta1lem2  21752  vieta1  21753  plyexmo  21754  elaa  21757  aannenlem1  21769  aalioulem2  21774  pilem1  21891  efif1olem3  21975  efif1olem4  21976  efifo  21978  eff1olem  21979  basellem4  22396  lgsqrlem2  22656  lgsqrlem3  22657  rpvmasum2  22736  dirith  22753  ofpreima  25935  qqhre  26398  indpi1  26430  indpreima  26433  sibfof  26678  cvmliftlem6  27131  cvmliftlem7  27132  cvmliftlem8  27133  cvmliftlem9  27134  itg2addnclem  28396  itg2addnclem2  28397  pw2f1o2val2  29342  dnnumch3  29353  proot1mul  29517  proot1hash  29521  proot1ex  29522  taupilem3  35452