Theorem fniniseg 7061

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1540   ∈ wcel 2105  {csn 4628  ^◡ccnv 5675   “ cima 5679   Fn wfn 6538  ‘cfv 6543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  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 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-fv 6551

This theorem is referenced by:  fparlem1  8102  fparlem2  8103  pw2f1olem  9080  recmulnq  10963  dmrecnq  10967  vdwlem1  16919  vdwlem2  16920  vdwlem6  16924  vdwlem8  16926  vdwlem9  16927  vdwlem12  16930  vdwlem13  16931  ramval  16946  ramub1lem1  16964  ghmeqker  19158  efgrelexlemb  19660  efgredeu  19662  psgnevpmb  21360  qtopeu  23441  itg1addlem1  25442  i1faddlem  25443  i1fmullem  25444  i1fmulclem  25453  i1fres  25456  itg10a  25461  itg1ge0a  25462  itg1climres  25465  mbfi1fseqlem4  25469  ply1remlem  25916  ply1rem  25917  fta1glem1  25919  fta1glem2  25920  fta1g  25921  fta1blem  25922  plyco0  25942  ofmulrt  26032  plyremlem  26054  plyrem  26055  fta1lem  26057  fta1  26058  vieta1lem1  26060  vieta1lem2  26061  vieta1  26062  plyexmo  26063  elaa  26066  aannenlem1  26078  aalioulem2  26083  pilem1  26200  efif1olem3  26290  efif1olem4  26291  efifo  26293  eff1olem  26294  basellem4  26825  lgsqrlem2  27087  lgsqrlem3  27088  rpvmasum2  27252  dirith  27269  foresf1o  32010  ofpreima  32158  fnpreimac  32164  1stpreimas  32195  s3clhash  32382  pwrssmgc  32438  cycpmconjslem2  32585  cyc3conja  32587  ghmquskerlem1  32803  ghmqusker  32807  dimkerim  33001  elirng  33040  irngss  33041  irngnzply1  33045  locfinreflem  33119  qqhre  33299  indpi1  33317  indpreima  33322  sibfof  33638  cvmliftlem6  34580  cvmliftlem7  34581  cvmliftlem8  34582  cvmliftlem9  34583  taupilem3  36504  itg2addnclem  36843  itg2addnclem2  36844  pw2f1o2val2  42082  dnnumch3  42092  proot1mul  42244  proot1hash  42245  proot1ex  42246  wessf1ornlem  44183  preimafvsnel  46346  uniimaprimaeqfv  46349  elsetpreimafvbi  46358