Theorem fniniseg 7041

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 7039	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵})))
2		fvex 6880	. . . 4 ⊢ (𝐹‘𝐶) ∈ V
3	2	elsn 4597	. . 3 ⊢ ((𝐹‘𝐶) ∈ {𝐵} ↔ (𝐹‘𝐶) = 𝐵)
4	3	anbi2i 632	. 2 ⊢ ((𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵))
5	1, 4	bitrdi 289	1 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1560   ∈ wcel 2142  {csn 4582  ^◡ccnv 5646   “ cima 5650   Fn wfn 6516  ‘cfv 6521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6477  df-fun 6523  df-fn 6524  df-fv 6529

This theorem is referenced by:  fparlem1  8091  fparlem2  8092  pw2f1olem  9053  recmulnq  10922  dmrecnq  10926  indpi1  12209  vdwlem1  17017  vdwlem2  17018  vdwlem6  17022  vdwlem8  17024  vdwlem9  17025  vdwlem12  17028  vdwlem13  17029  ramval  17044  ramub1lem1  17062  ghmeqker  19283  ghmqusnsglem1  19320  ghmquskerlem1  19323  ghmqusker  19327  efgrelexlemb  19790  efgredeu  19792  psgnevpmb  21636  qtopeu  23773  itg1addlem1  25751  i1faddlem  25752  i1fmullem  25753  i1fmulclem  25761  i1fres  25764  itg10a  25769  itg1ge0a  25770  itg1climres  25773  mbfi1fseqlem4  25777  ply1remlem  26222  ply1rem  26223  fta1glem1  26225  fta1glem2  26226  fta1g  26227  fta1blem  26228  plyco0  26249  ofmulrt  26340  plyremlem  26365  plyrem  26366  fta1lem  26368  fta1  26369  vieta1lem1  26371  vieta1lem2  26372  vieta1  26373  plyexmo  26374  elaa  26377  aannenlem1  26389  aalioulem2  26394  pilem1  26511  efif1olem3  26606  efif1olem4  26607  efifo  26609  eff1olem  26610  basellem4  27145  lgsqrlem2  27408  lgsqrlem3  27409  rpvmasum2  27573  dirith  27590  foresf1o  32700  ofpreima  32864  fnpreimac  32869  1stpreimas  32905  indpreima  33040  s3clhash  33123  pwrssmgc  33175  cycpmconjslem2  33332  cyc3conja  33334  exsslsb  33891  dimkerim  33921  elirng  33980  irngss  33981  irngnzply1  33985  locfinreflem  34134  qqhre  34314  sibfof  34634  cvmliftlem6  35637  cvmliftlem7  35638  cvmliftlem8  35639  cvmliftlem9  35640  taupilem3  37808  itg2addnclem  38167  itg2addnclem2  38168  pw2f1o2val2  43614  dnnumch3  43621  proot1mul  43768  proot1hash  43769  proot1ex  43770  wessf1ornlem  45760  preimafvsnel  47982  uniimaprimaeqfv  47985  elsetpreimafvbi  47994  imasubc  49769  imassc  49771  imaid  49772