Theorem fniniseg 7012

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {csn 4567  ^◡ccnv 5630   “ cima 5634   Fn wfn 6493  ‘cfv 6498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-fv 6506

This theorem is referenced by:  fparlem1  8062  fparlem2  8063  pw2f1olem  9019  recmulnq  10887  dmrecnq  10891  indpi1  12173  vdwlem1  16952  vdwlem2  16953  vdwlem6  16957  vdwlem8  16959  vdwlem9  16960  vdwlem12  16963  vdwlem13  16964  ramval  16979  ramub1lem1  16997  ghmeqker  19218  ghmqusnsglem1  19255  ghmquskerlem1  19258  ghmqusker  19262  efgrelexlemb  19725  efgredeu  19727  psgnevpmb  21567  qtopeu  23681  itg1addlem1  25659  i1faddlem  25660  i1fmullem  25661  i1fmulclem  25669  i1fres  25672  itg10a  25677  itg1ge0a  25678  itg1climres  25681  mbfi1fseqlem4  25685  ply1remlem  26130  ply1rem  26131  fta1glem1  26133  fta1glem2  26134  fta1g  26135  fta1blem  26136  plyco0  26157  ofmulrt  26248  plyremlem  26270  plyrem  26271  fta1lem  26273  fta1  26274  vieta1lem1  26276  vieta1lem2  26277  vieta1  26278  plyexmo  26279  elaa  26282  aannenlem1  26294  aalioulem2  26299  pilem1  26416  efif1olem3  26508  efif1olem4  26509  efifo  26511  eff1olem  26512  basellem4  27047  lgsqrlem2  27310  lgsqrlem3  27311  rpvmasum2  27475  dirith  27492  foresf1o  32574  ofpreima  32738  fnpreimac  32743  1stpreimas  32779  indpreima  32925  s3clhash  33008  pwrssmgc  33060  cycpmconjslem2  33216  cyc3conja  33218  exsslsb  33741  dimkerim  33771  elirng  33830  irngss  33831  irngnzply1  33835  locfinreflem  33984  qqhre  34164  sibfof  34484  cvmliftlem6  35472  cvmliftlem7  35473  cvmliftlem8  35474  cvmliftlem9  35475  taupilem3  37633  itg2addnclem  37992  itg2addnclem2  37993  pw2f1o2val2  43468  dnnumch3  43475  proot1mul  43622  proot1hash  43623  proot1ex  43624  wessf1ornlem  45615  preimafvsnel  47839  uniimaprimaeqfv  47842  elsetpreimafvbi  47851  imasubc  49626  imassc  49628  imaid  49629