Theorem fniniseg 7059

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2146  {csn 4591  ^◡ccnv 5662   “ cima 5666   Fn wfn 6535  ‘cfv 6540

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-fv 6548

This theorem is used by:  fparlem1  8113  fparlem2  8114  pw2f1olem  9076  recmulnq  10964  dmrecnq  10968  indpi1  12247  vdwlem1  17063  vdwlem2  17064  vdwlem6  17068  vdwlem8  17070  vdwlem9  17071  vdwlem12  17074  vdwlem13  17075  ramval  17090  ramub1lem1  17108  ghmeqker  19357  ghmqusnsglem1  19394  ghmquskerlem1  19397  ghmqusker  19401  efgrelexlemb  19864  efgredeu  19866  psgnevpmb  21787  qtopeu  23924  itg1addlem1  25902  i1faddlem  25903  i1fmullem  25904  i1fmulclem  25912  i1fres  25915  itg10a  25920  itg1ge0a  25921  itg1climres  25924  mbfi1fseqlem4  25928  ply1remlem  26373  ply1rem  26374  fta1glem1  26376  fta1glem2  26377  fta1g  26378  fta1blem  26379  plyco0  26400  ofmulrt  26491  plyremlem  26516  plyrem  26517  fta1lem  26519  fta1  26520  vieta1lem1  26522  vieta1lem2  26523  vieta1  26524  plyexmo  26525  elaa  26528  aannenlem1  26542  aalioulem2  26547  pilem1  26665  efif1olem3  26760  efif1olem4  26761  efifo  26763  eff1olem  26764  basellem4  27299  lgsqrlem2  27562  lgsqrlem3  27563  rpvmasum2  27727  dirith  27744  foresf1o  32921  ofpreima  33081  fnpreimac  33086  1stpreimas  33122  indpreima  33255  s3clhash  33335  pwrssmgc  33384  cycpmconjslem2  33539  cyc3conja  33541  exsslsb  34051  dimkerim  34081  elirng  34140  irngss  34141  irngnzply1  34145  locfinreflem  34294  qqhre  34474  sibfof  34795  cvmliftlem6  35819  cvmliftlem7  35820  cvmliftlem8  35821  cvmliftlem9  35822  taupilem3  38020  itg2addnclem  38379  itg2addnclem2  38380  pw2f1o2val2  43825  dnnumch3  43832  proot1mul  43979  proot1hash  43980  proot1ex  43981  wessf1ornlem  45961  preimafvsnel  48186  uniimaprimaeqfv  48189  elsetpreimafvbi  48198  imasubc  49986  imassc  49988  imaid  49989