Theorem fniniseg 5984

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 5983	. 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 4040	. . 3 |- ( ( F ` C ) e. { B } <-> ( F ` C ) = B )
4	3	anbi2i 692	. 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 367   = wceq 1398   e. wcel 1823   {csn 4016   `'ccnv 4987   "cima 4991   Fn wfn 5565   ` cfv 5570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-fv 5578

This theorem is referenced by:  fparlem1  6873  fparlem2  6874  pw2f1olem  7614  recmulnq  9331  dmrecnq  9335  vdwlem1  14583  vdwlem2  14584  vdwlem6  14588  vdwlem8  14590  vdwlem9  14591  vdwlem12  14594  vdwlem13  14595  ramval  14610  ramub1lem1  14628  ghmeqker  16492  efgrelexlemb  16967  efgredeu  16969  psgnevpmb  18796  qtopeu  20383  itg1addlem1  22265  i1faddlem  22266  i1fmullem  22267  i1fmulclem  22275  i1fres  22278  itg10a  22283  itg1ge0a  22284  itg1climres  22287  mbfi1fseqlem4  22291  ply1remlem  22729  ply1rem  22730  fta1glem1  22732  fta1glem2  22733  fta1g  22734  fta1blem  22735  plyco0  22755  ofmulrt  22844  plyremlem  22866  plyrem  22867  fta1lem  22869  fta1  22870  vieta1lem1  22872  vieta1lem2  22873  vieta1  22874  plyexmo  22875  elaa  22878  aannenlem1  22890  aalioulem2  22895  pilem1  23012  efif1olem3  23097  efif1olem4  23098  efifo  23100  eff1olem  23101  basellem4  23555  lgsqrlem2  23815  lgsqrlem3  23816  rpvmasum2  23895  dirith  23912  foresf1o  27602  ofpreima  27734  1stpreimas  27752  locfinreflem  28078  qqhre  28232  indpi1  28251  indpreima  28254  sibfof  28546  cvmliftlem6  28999  cvmliftlem7  29000  cvmliftlem8  29001  cvmliftlem9  29002  itg2addnclem  30306  itg2addnclem2  30307  pw2f1o2val2  31221  dnnumch3  31232  proot1mul  31397  proot1hash  31401  proot1ex  31402  taupilem3  38091