Theorem fniniseg 7061

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  {csn 4628  ^◡ccnv 5675   “ cima 5679   Fn wfn 6538  ‘cfv 6543

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-fv 6551

This theorem is referenced by:  fparlem1  8100  fparlem2  8101  pw2f1olem  9078  recmulnq  10961  dmrecnq  10965  vdwlem1  16916  vdwlem2  16917  vdwlem6  16921  vdwlem8  16923  vdwlem9  16924  vdwlem12  16927  vdwlem13  16928  ramval  16943  ramub1lem1  16961  ghmeqker  19121  efgrelexlemb  19620  efgredeu  19622  psgnevpmb  21146  qtopeu  23227  itg1addlem1  25216  i1faddlem  25217  i1fmullem  25218  i1fmulclem  25227  i1fres  25230  itg10a  25235  itg1ge0a  25236  itg1climres  25239  mbfi1fseqlem4  25243  ply1remlem  25687  ply1rem  25688  fta1glem1  25690  fta1glem2  25691  fta1g  25692  fta1blem  25693  plyco0  25713  ofmulrt  25802  plyremlem  25824  plyrem  25825  fta1lem  25827  fta1  25828  vieta1lem1  25830  vieta1lem2  25831  vieta1  25832  plyexmo  25833  elaa  25836  aannenlem1  25848  aalioulem2  25853  pilem1  25970  efif1olem3  26060  efif1olem4  26061  efifo  26063  eff1olem  26064  basellem4  26595  lgsqrlem2  26857  lgsqrlem3  26858  rpvmasum2  27022  dirith  27039  foresf1o  31780  ofpreima  31928  fnpreimac  31934  1stpreimas  31965  s3clhash  32152  pwrssmgc  32208  cycpmconjslem2  32355  cyc3conja  32357  ghmquskerlem1  32573  ghmqusker  32577  dimkerim  32771  elirng  32810  irngss  32811  irngnzply1  32815  locfinreflem  32889  qqhre  33069  indpi1  33087  indpreima  33092  sibfof  33408  cvmliftlem6  34350  cvmliftlem7  34351  cvmliftlem8  34352  cvmliftlem9  34353  taupilem3  36286  itg2addnclem  36625  itg2addnclem2  36626  pw2f1o2val2  41861  dnnumch3  41871  proot1mul  42023  proot1hash  42024  proot1ex  42025  wessf1ornlem  43963  preimafvsnel  46126  uniimaprimaeqfv  46129  elsetpreimafvbi  46138