Theorem fniniseg 7056

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 7054	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵})))
2		fvex 6895	. . . 4 ⊢ (𝐹‘𝐶) ∈ V
3	2	elsn 4609	. . 3 ⊢ ((𝐹‘𝐶) ∈ {𝐵} ↔ (𝐹‘𝐶) = 𝐵)
4	3	anbi2i 634	. 2 ⊢ ((𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵))
5	1, 4	bitrdi 290	1 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567   ∈ wcel 2149  {csn 4594  ^◡ccnv 5661   “ cima 5665   Fn wfn 6532  ‘cfv 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-fv 6545

This theorem is referenced by:  fparlem1  8106  fparlem2  8107  pw2f1olem  9068  recmulnq  10948  dmrecnq  10952  indpi1  12231  vdwlem1  17040  vdwlem2  17041  vdwlem6  17045  vdwlem8  17047  vdwlem9  17048  vdwlem12  17051  vdwlem13  17052  ramval  17067  ramub1lem1  17085  ghmeqker  19312  ghmqusnsglem1  19349  ghmquskerlem1  19352  ghmqusker  19356  efgrelexlemb  19819  efgredeu  19821  psgnevpmb  21705  qtopeu  23841  itg1addlem1  25819  i1faddlem  25820  i1fmullem  25821  i1fmulclem  25829  i1fres  25832  itg10a  25837  itg1ge0a  25838  itg1climres  25841  mbfi1fseqlem4  25845  ply1remlem  26290  ply1rem  26291  fta1glem1  26293  fta1glem2  26294  fta1g  26295  fta1blem  26296  plyco0  26317  ofmulrt  26408  plyremlem  26433  plyrem  26434  fta1lem  26436  fta1  26437  vieta1lem1  26439  vieta1lem2  26440  vieta1  26441  plyexmo  26442  elaa  26445  aannenlem1  26457  aalioulem2  26462  pilem1  26579  efif1olem3  26674  efif1olem4  26675  efifo  26677  eff1olem  26678  basellem4  27213  lgsqrlem2  27476  lgsqrlem3  27477  rpvmasum2  27641  dirith  27658  foresf1o  32790  ofpreima  32950  fnpreimac  32955  1stpreimas  32991  indpreima  33125  s3clhash  33208  pwrssmgc  33260  cycpmconjslem2  33415  cyc3conja  33417  exsslsb  33931  dimkerim  33961  elirng  34020  irngss  34021  irngnzply1  34025  locfinreflem  34174  qqhre  34354  sibfof  34674  cvmliftlem6  35680  cvmliftlem7  35681  cvmliftlem8  35682  cvmliftlem9  35683  taupilem3  37850  itg2addnclem  38209  itg2addnclem2  38210  pw2f1o2val2  43658  dnnumch3  43665  proot1mul  43812  proot1hash  43813  proot1ex  43814  wessf1ornlem  45794  preimafvsnel  48016  uniimaprimaeqfv  48019  elsetpreimafvbi  48028  imasubc  49813  imassc  49815  imaid  49816