Theorem fniniseg 7014

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 7012	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵})))
2		fvex 6853	. . . 4 ⊢ (𝐹‘𝐶) ∈ V
3	2	elsn 4600	. . 3 ⊢ ((𝐹‘𝐶) ∈ {𝐵} ↔ (𝐹‘𝐶) = 𝐵)
4	3	anbi2i 623	. 2 ⊢ ((𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵))
5	1, 4	bitrdi 287	1 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {csn 4585  ^◡ccnv 5630   “ cima 5634   Fn wfn 6494  ‘cfv 6499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-fv 6507

This theorem is referenced by:  fparlem1  8068  fparlem2  8069  pw2f1olem  9022  recmulnq  10893  dmrecnq  10897  vdwlem1  16928  vdwlem2  16929  vdwlem6  16933  vdwlem8  16935  vdwlem9  16936  vdwlem12  16939  vdwlem13  16940  ramval  16955  ramub1lem1  16973  ghmeqker  19157  ghmqusnsglem1  19194  ghmquskerlem1  19197  ghmqusker  19201  efgrelexlemb  19664  efgredeu  19666  psgnevpmb  21529  qtopeu  23636  itg1addlem1  25626  i1faddlem  25627  i1fmullem  25628  i1fmulclem  25636  i1fres  25639  itg10a  25644  itg1ge0a  25645  itg1climres  25648  mbfi1fseqlem4  25652  ply1remlem  26103  ply1rem  26104  fta1glem1  26106  fta1glem2  26107  fta1g  26108  fta1blem  26109  plyco0  26130  ofmulrt  26222  plyremlem  26245  plyrem  26246  fta1lem  26248  fta1  26249  vieta1lem1  26251  vieta1lem2  26252  vieta1  26253  plyexmo  26254  elaa  26257  aannenlem1  26269  aalioulem2  26274  pilem1  26394  efif1olem3  26486  efif1olem4  26487  efifo  26489  eff1olem  26490  basellem4  27027  lgsqrlem2  27291  lgsqrlem3  27292  rpvmasum2  27456  dirith  27473  foresf1o  32483  ofpreima  32639  fnpreimac  32645  1stpreimas  32679  indpi1  32833  indpreima  32838  s3clhash  32919  pwrssmgc  32972  cycpmconjslem2  33127  cyc3conja  33129  exsslsb  33585  dimkerim  33616  elirng  33674  irngss  33675  irngnzply1  33679  locfinreflem  33823  qqhre  34003  sibfof  34324  cvmliftlem6  35270  cvmliftlem7  35271  cvmliftlem8  35272  cvmliftlem9  35273  taupilem3  37300  itg2addnclem  37658  itg2addnclem2  37659  pw2f1o2val2  43022  dnnumch3  43029  proot1mul  43176  proot1hash  43177  proot1ex  43178  wessf1ornlem  45172  preimafvsnel  47373  uniimaprimaeqfv  47376  elsetpreimafvbi  47385  imasubc  49133  imassc  49135  imaid  49136