Theorem fniniseg 7015

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  {csn 4591  ^◡ccnv 5637   “ cima 5641   Fn wfn 6496  ‘cfv 6501

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fn 6504  df-fv 6509

This theorem is referenced by:  fparlem1  8049  fparlem2  8050  pw2f1olem  9027  recmulnq  10909  dmrecnq  10913  vdwlem1  16864  vdwlem2  16865  vdwlem6  16869  vdwlem8  16871  vdwlem9  16872  vdwlem12  16875  vdwlem13  16876  ramval  16891  ramub1lem1  16909  ghmeqker  19049  efgrelexlemb  19546  efgredeu  19548  psgnevpmb  21028  qtopeu  23104  itg1addlem1  25093  i1faddlem  25094  i1fmullem  25095  i1fmulclem  25104  i1fres  25107  itg10a  25112  itg1ge0a  25113  itg1climres  25116  mbfi1fseqlem4  25120  ply1remlem  25564  ply1rem  25565  fta1glem1  25567  fta1glem2  25568  fta1g  25569  fta1blem  25570  plyco0  25590  ofmulrt  25679  plyremlem  25701  plyrem  25702  fta1lem  25704  fta1  25705  vieta1lem1  25707  vieta1lem2  25708  vieta1  25709  plyexmo  25710  elaa  25713  aannenlem1  25725  aalioulem2  25730  pilem1  25847  efif1olem3  25937  efif1olem4  25938  efifo  25940  eff1olem  25941  basellem4  26470  lgsqrlem2  26732  lgsqrlem3  26733  rpvmasum2  26897  dirith  26914  foresf1o  31495  ofpreima  31648  fnpreimac  31654  1stpreimas  31687  s3clhash  31874  pwrssmgc  31930  cycpmconjslem2  32074  cyc3conja  32076  ghmquskerlem1  32269  ghmqusker  32272  dimkerim  32409  elirng  32447  irngss  32448  irngnzply1  32452  locfinreflem  32510  qqhre  32690  indpi1  32708  indpreima  32713  sibfof  33029  cvmliftlem6  33971  cvmliftlem7  33972  cvmliftlem8  33973  cvmliftlem9  33974  taupilem3  35863  itg2addnclem  36202  itg2addnclem2  36203  pw2f1o2val2  41422  dnnumch3  41432  proot1mul  41584  proot1hash  41585  proot1ex  41586  wessf1ornlem  43525  preimafvsnel  45691  uniimaprimaeqfv  45694  elsetpreimafvbi  45703