Theorem fniniseg 7079

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1536   ∈ wcel 2105  {csn 4630  ^◡ccnv 5687   “ cima 5691   Fn wfn 6557  ‘cfv 6562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-fv 6570

This theorem is referenced by:  fparlem1  8135  fparlem2  8136  pw2f1olem  9114  recmulnq  11001  dmrecnq  11005  vdwlem1  17014  vdwlem2  17015  vdwlem6  17019  vdwlem8  17021  vdwlem9  17022  vdwlem12  17025  vdwlem13  17026  ramval  17041  ramub1lem1  17059  ghmeqker  19273  ghmqusnsglem1  19310  ghmquskerlem1  19313  ghmqusker  19317  efgrelexlemb  19782  efgredeu  19784  psgnevpmb  21622  qtopeu  23739  itg1addlem1  25740  i1faddlem  25741  i1fmullem  25742  i1fmulclem  25751  i1fres  25754  itg10a  25759  itg1ge0a  25760  itg1climres  25763  mbfi1fseqlem4  25767  ply1remlem  26218  ply1rem  26219  fta1glem1  26221  fta1glem2  26222  fta1g  26223  fta1blem  26224  plyco0  26245  ofmulrt  26337  plyremlem  26360  plyrem  26361  fta1lem  26363  fta1  26364  vieta1lem1  26366  vieta1lem2  26367  vieta1  26368  plyexmo  26369  elaa  26372  aannenlem1  26384  aalioulem2  26389  pilem1  26509  efif1olem3  26600  efif1olem4  26601  efifo  26603  eff1olem  26604  basellem4  27141  lgsqrlem2  27405  lgsqrlem3  27406  rpvmasum2  27570  dirith  27587  foresf1o  32531  ofpreima  32681  fnpreimac  32687  1stpreimas  32720  s3clhash  32916  pwrssmgc  32974  cycpmconjslem2  33157  cyc3conja  33159  dimkerim  33654  elirng  33700  irngss  33701  irngnzply1  33705  locfinreflem  33800  qqhre  33982  indpi1  34000  indpreima  34005  sibfof  34321  cvmliftlem6  35274  cvmliftlem7  35275  cvmliftlem8  35276  cvmliftlem9  35277  taupilem3  37301  itg2addnclem  37657  itg2addnclem2  37658  pw2f1o2val2  43028  dnnumch3  43035  proot1mul  43182  proot1hash  43183  proot1ex  43184  wessf1ornlem  45127  preimafvsnel  47303  uniimaprimaeqfv  47306  elsetpreimafvbi  47315