Theorem fniniseg 6937

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2106  {csn 4561  ^◡ccnv 5588   “ cima 5592   Fn wfn 6428  ‘cfv 6433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-fv 6441

This theorem is referenced by:  fparlem1  7952  fparlem2  7953  pw2f1olem  8863  recmulnq  10720  dmrecnq  10724  vdwlem1  16682  vdwlem2  16683  vdwlem6  16687  vdwlem8  16689  vdwlem9  16690  vdwlem12  16693  vdwlem13  16694  ramval  16709  ramub1lem1  16727  ghmeqker  18861  efgrelexlemb  19356  efgredeu  19358  psgnevpmb  20792  qtopeu  22867  itg1addlem1  24856  i1faddlem  24857  i1fmullem  24858  i1fmulclem  24867  i1fres  24870  itg10a  24875  itg1ge0a  24876  itg1climres  24879  mbfi1fseqlem4  24883  ply1remlem  25327  ply1rem  25328  fta1glem1  25330  fta1glem2  25331  fta1g  25332  fta1blem  25333  plyco0  25353  ofmulrt  25442  plyremlem  25464  plyrem  25465  fta1lem  25467  fta1  25468  vieta1lem1  25470  vieta1lem2  25471  vieta1  25472  plyexmo  25473  elaa  25476  aannenlem1  25488  aalioulem2  25493  pilem1  25610  efif1olem3  25700  efif1olem4  25701  efifo  25703  eff1olem  25704  basellem4  26233  lgsqrlem2  26495  lgsqrlem3  26496  rpvmasum2  26660  dirith  26677  foresf1o  30850  ofpreima  31002  fnpreimac  31008  1stpreimas  31038  s3clhash  31222  pwrssmgc  31278  cycpmconjslem2  31422  cyc3conja  31424  dimkerim  31708  locfinreflem  31790  qqhre  31970  indpi1  31988  indpreima  31993  sibfof  32307  cvmliftlem6  33252  cvmliftlem7  33253  cvmliftlem8  33254  cvmliftlem9  33255  taupilem3  35490  itg2addnclem  35828  itg2addnclem2  35829  pw2f1o2val2  40862  dnnumch3  40872  proot1mul  41024  proot1hash  41025  proot1ex  41026  wessf1ornlem  42722  preimafvsnel  44831  uniimaprimaeqfv  44834  elsetpreimafvbi  44843