Theorem fniniseg 7003

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	⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵)))

Proof of Theorem fniniseg

Step	Hyp	Ref	Expression
1		elpreima 7001	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵})))
2		fvex 6845	. . . 4 ⊢ (𝐹‘𝐶) ∈ V
3	2	elsn 4593	. . 3 ⊢ ((𝐹‘𝐶) ∈ {𝐵} ↔ (𝐹‘𝐶) = 𝐵)
4	3	anbi2i 623	. 2 ⊢ ((𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵))
5	1, 4	bitrdi 287	1 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  {csn 4578  ^◡ccnv 5621   “ cima 5625   Fn wfn 6485  ‘cfv 6490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-fv 6498

This theorem is referenced by:  fparlem1  8052  fparlem2  8053  pw2f1olem  9007  recmulnq  10873  dmrecnq  10877  vdwlem1  16907  vdwlem2  16908  vdwlem6  16912  vdwlem8  16914  vdwlem9  16915  vdwlem12  16918  vdwlem13  16919  ramval  16934  ramub1lem1  16952  ghmeqker  19170  ghmqusnsglem1  19207  ghmquskerlem1  19210  ghmqusker  19214  efgrelexlemb  19677  efgredeu  19679  psgnevpmb  21540  qtopeu  23658  itg1addlem1  25647  i1faddlem  25648  i1fmullem  25649  i1fmulclem  25657  i1fres  25660  itg10a  25665  itg1ge0a  25666  itg1climres  25669  mbfi1fseqlem4  25673  ply1remlem  26124  ply1rem  26125  fta1glem1  26127  fta1glem2  26128  fta1g  26129  fta1blem  26130  plyco0  26151  ofmulrt  26243  plyremlem  26266  plyrem  26267  fta1lem  26269  fta1  26270  vieta1lem1  26272  vieta1lem2  26273  vieta1  26274  plyexmo  26275  elaa  26278  aannenlem1  26290  aalioulem2  26295  pilem1  26415  efif1olem3  26507  efif1olem4  26508  efifo  26510  eff1olem  26511  basellem4  27048  lgsqrlem2  27312  lgsqrlem3  27313  rpvmasum2  27477  dirith  27494  foresf1o  32528  ofpreima  32692  fnpreimac  32698  1stpreimas  32734  indpi1  32890  indpreima  32896  s3clhash  32979  pwrssmgc  33031  cycpmconjslem2  33186  cyc3conja  33188  exsslsb  33702  dimkerim  33733  elirng  33792  irngss  33793  irngnzply1  33797  locfinreflem  33946  qqhre  34126  sibfof  34446  cvmliftlem6  35433  cvmliftlem7  35434  cvmliftlem8  35435  cvmliftlem9  35436  taupilem3  37463  itg2addnclem  37811  itg2addnclem2  37812  pw2f1o2val2  43224  dnnumch3  43231  proot1mul  43378  proot1hash  43379  proot1ex  43380  wessf1ornlem  45371  preimafvsnel  47567  uniimaprimaeqfv  47570  elsetpreimafvbi  47579  imasubc  49338  imassc  49340  imaid  49341