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  19151  ghmqusnsglem1  19188  ghmquskerlem1  19191  ghmqusker  19195  efgrelexlemb  19656  efgredeu  19658  psgnevpmb  21472  qtopeu  23579  itg1addlem1  25569  i1faddlem  25570  i1fmullem  25571  i1fmulclem  25579  i1fres  25582  itg10a  25587  itg1ge0a  25588  itg1climres  25591  mbfi1fseqlem4  25595  ply1remlem  26046  ply1rem  26047  fta1glem1  26049  fta1glem2  26050  fta1g  26051  fta1blem  26052  plyco0  26073  ofmulrt  26165  plyremlem  26188  plyrem  26189  fta1lem  26191  fta1  26192  vieta1lem1  26194  vieta1lem2  26195  vieta1  26196  plyexmo  26197  elaa  26200  aannenlem1  26212  aalioulem2  26217  pilem1  26337  efif1olem3  26429  efif1olem4  26430  efifo  26432  eff1olem  26433  basellem4  26970  lgsqrlem2  27234  lgsqrlem3  27235  rpvmasum2  27399  dirith  27416  foresf1o  32406  ofpreima  32562  fnpreimac  32568  1stpreimas  32602  indpi1  32756  indpreima  32761  s3clhash  32842  pwrssmgc  32899  cycpmconjslem2  33085  cyc3conja  33087  exsslsb  33565  dimkerim  33596  elirng  33654  irngss  33655  irngnzply1  33659  locfinreflem  33803  qqhre  33983  sibfof  34304  cvmliftlem6  35250  cvmliftlem7  35251  cvmliftlem8  35252  cvmliftlem9  35253  taupilem3  37280  itg2addnclem  37638  itg2addnclem2  37639  pw2f1o2val2  43002  dnnumch3  43009  proot1mul  43156  proot1hash  43157  proot1ex  43158  wessf1ornlem  45152  preimafvsnel  47353  uniimaprimaeqfv  47356  elsetpreimafvbi  47365  imasubc  49113  imassc  49115  imaid  49116