Theorem fniniseg 7005

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 7003	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵})))
2		fvex 6847	. . . 4 ⊢ (𝐹‘𝐶) ∈ V
3	2	elsn 4595	. . 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 4580  ^◡ccnv 5623   “ cima 5627   Fn wfn 6487  ‘cfv 6492

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 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-fv 6500

This theorem is referenced by:  fparlem1  8054  fparlem2  8055  pw2f1olem  9009  recmulnq  10875  dmrecnq  10879  vdwlem1  16909  vdwlem2  16910  vdwlem6  16914  vdwlem8  16916  vdwlem9  16917  vdwlem12  16920  vdwlem13  16921  ramval  16936  ramub1lem1  16954  ghmeqker  19172  ghmqusnsglem1  19209  ghmquskerlem1  19212  ghmqusker  19216  efgrelexlemb  19679  efgredeu  19681  psgnevpmb  21542  qtopeu  23660  itg1addlem1  25649  i1faddlem  25650  i1fmullem  25651  i1fmulclem  25659  i1fres  25662  itg10a  25667  itg1ge0a  25668  itg1climres  25671  mbfi1fseqlem4  25675  ply1remlem  26126  ply1rem  26127  fta1glem1  26129  fta1glem2  26130  fta1g  26131  fta1blem  26132  plyco0  26153  ofmulrt  26245  plyremlem  26268  plyrem  26269  fta1lem  26271  fta1  26272  vieta1lem1  26274  vieta1lem2  26275  vieta1  26276  plyexmo  26277  elaa  26280  aannenlem1  26292  aalioulem2  26297  pilem1  26417  efif1olem3  26509  efif1olem4  26510  efifo  26512  eff1olem  26513  basellem4  27050  lgsqrlem2  27314  lgsqrlem3  27315  rpvmasum2  27479  dirith  27496  foresf1o  32579  ofpreima  32743  fnpreimac  32749  1stpreimas  32785  indpi1  32941  indpreima  32947  s3clhash  33030  pwrssmgc  33082  cycpmconjslem2  33237  cyc3conja  33239  exsslsb  33753  dimkerim  33784  elirng  33843  irngss  33844  irngnzply1  33848  locfinreflem  33997  qqhre  34177  sibfof  34497  cvmliftlem6  35484  cvmliftlem7  35485  cvmliftlem8  35486  cvmliftlem9  35487  taupilem3  37524  itg2addnclem  37872  itg2addnclem2  37873  pw2f1o2val2  43282  dnnumch3  43289  proot1mul  43436  proot1hash  43437  proot1ex  43438  wessf1ornlem  45429  preimafvsnel  47625  uniimaprimaeqfv  47628  elsetpreimafvbi  47637  imasubc  49396  imassc  49398  imaid  49399