Theorem fniniseg 5932

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 5931	. 2 |- ( F Fn A -> ( C e. ( `' F " { B } ) <-> ( C e. A /\ ( F ` C ) e. { B } ) ) )
2		fvex 5808	. . . 4 |- ( F ` C ) e. _V
3	2	elsnc 4008	. . 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 1370   e. wcel 1758   {csn 3984   `'ccnv 4946   "cima 4950   Fn wfn 5520   ` cfv 5525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4520  ax-nul 4528  ax-pr 4638

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-ral 2803  df-rex 2804  df-rab 2807  df-v 3078  df-sbc 3293  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-sn 3985  df-pr 3987  df-op 3991  df-uni 4199  df-br 4400  df-opab 4458  df-id 4743  df-xp 4953  df-rel 4954  df-cnv 4955  df-co 4956  df-dm 4957  df-rn 4958  df-res 4959  df-ima 4960  df-iota 5488  df-fun 5527  df-fn 5528  df-fv 5533

This theorem is referenced by:  fparlem1  6781  fparlem2  6782  pw2f1olem  7524  recmulnq  9243  dmrecnq  9247  vdwlem1  14159  vdwlem2  14160  vdwlem6  14164  vdwlem8  14166  vdwlem9  14167  vdwlem12  14170  vdwlem13  14171  ramval  14186  ramub1lem1  14204  ghmeqker  15891  efgrelexlemb  16367  efgredeu  16369  psgnevpmb  18141  qtopeu  19420  itg1addlem1  21302  i1faddlem  21303  i1fmullem  21304  i1fmulclem  21312  i1fres  21315  itg10a  21320  itg1ge0a  21321  itg1climres  21324  mbfi1fseqlem4  21328  ply1remlem  21766  ply1rem  21767  fta1glem1  21769  fta1glem2  21770  fta1g  21771  fta1blem  21772  plyco0  21792  ofmulrt  21880  plyremlem  21902  plyrem  21903  fta1lem  21905  fta1  21906  vieta1lem1  21908  vieta1lem2  21909  vieta1  21910  plyexmo  21911  elaa  21914  aannenlem1  21926  aalioulem2  21931  pilem1  22048  efif1olem3  22132  efif1olem4  22133  efifo  22135  eff1olem  22136  basellem4  22553  lgsqrlem2  22813  lgsqrlem3  22814  rpvmasum2  22893  dirith  22910  ofpreima  26134  qqhre  26590  indpi1  26622  indpreima  26625  sibfof  26869  cvmliftlem6  27322  cvmliftlem7  27323  cvmliftlem8  27324  cvmliftlem9  27325  itg2addnclem  28590  itg2addnclem2  28591  pw2f1o2val2  29536  dnnumch3  29547  proot1mul  29711  proot1hash  29715  proot1ex  29716  taupilem3  35935