Theorem fniniseg 6654

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 6652	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵})))
2		fvex 6510	. . . 4 ⊢ (𝐹‘𝐶) ∈ V
3	2	elsn 4451	. . 3 ⊢ ((𝐹‘𝐶) ∈ {𝐵} ↔ (𝐹‘𝐶) = 𝐵)
4	3	anbi2i 614	. 2 ⊢ ((𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵))
5	1, 4	syl6bb 279	1 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵)))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387   = wceq 1508   ∈ wcel 2051  {csn 4436  ^◡ccnv 5403   “ cima 5407   Fn wfn 6181  ‘cfv 6186

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2745  ax-sep 5057  ax-nul 5064  ax-pr 5183

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ne 2963  df-ral 3088  df-rex 3089  df-rab 3092  df-v 3412  df-sbc 3677  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-nul 4174  df-if 4346  df-sn 4437  df-pr 4439  df-op 4443  df-uni 4710  df-br 4927  df-opab 4989  df-id 5309  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-iota 6150  df-fun 6188  df-fn 6189  df-fv 6194

This theorem is referenced by:  fparlem1  7614  fparlem2  7615  pw2f1olem  8416  recmulnq  10183  dmrecnq  10187  vdwlem1  16172  vdwlem2  16173  vdwlem6  16177  vdwlem8  16179  vdwlem9  16180  vdwlem12  16183  vdwlem13  16184  ramval  16199  ramub1lem1  16217  ghmeqker  18169  efgrelexlemb  18649  efgredeu  18651  psgnevpmb  20449  qtopeu  22044  itg1addlem1  24012  i1faddlem  24013  i1fmullem  24014  i1fmulclem  24022  i1fres  24025  itg10a  24030  itg1ge0a  24031  itg1climres  24034  mbfi1fseqlem4  24038  ply1remlem  24475  ply1rem  24476  fta1glem1  24478  fta1glem2  24479  fta1g  24480  fta1blem  24481  plyco0  24501  ofmulrt  24590  plyremlem  24612  plyrem  24613  fta1lem  24615  fta1  24616  vieta1lem1  24618  vieta1lem2  24619  vieta1  24620  plyexmo  24621  elaa  24624  aannenlem1  24636  aalioulem2  24641  pilem1  24758  efif1olem3  24845  efif1olem4  24846  efifo  24848  eff1olem  24849  basellem4  25379  lgsqrlem2  25641  lgsqrlem3  25642  rpvmasum2  25806  dirith  25823  foresf1o  30060  ofpreima  30190  fnpreimac  30196  1stpreimas  30218  s3clhash  30391  dimkerim  30685  locfinreflem  30781  qqhre  30938  indpi1  30956  indpreima  30961  sibfof  31276  cvmliftlem6  32155  cvmliftlem7  32156  cvmliftlem8  32157  cvmliftlem9  32158  taupilem3  34075  itg2addnclem  34417  itg2addnclem2  34418  pw2f1o2val2  39067  dnnumch3  39077  proot1mul  39229  proot1hash  39230  proot1ex  39231  wessf1ornlem  40900