Theorem fniniseg 6919

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539   ∈ wcel 2108  {csn 4558  ^◡ccnv 5579   “ cima 5583   Fn wfn 6413  ‘cfv 6418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-fv 6426

This theorem is referenced by:  fparlem1  7923  fparlem2  7924  pw2f1olem  8816  recmulnq  10651  dmrecnq  10655  vdwlem1  16610  vdwlem2  16611  vdwlem6  16615  vdwlem8  16617  vdwlem9  16618  vdwlem12  16621  vdwlem13  16622  ramval  16637  ramub1lem1  16655  ghmeqker  18776  efgrelexlemb  19271  efgredeu  19273  psgnevpmb  20704  qtopeu  22775  itg1addlem1  24761  i1faddlem  24762  i1fmullem  24763  i1fmulclem  24772  i1fres  24775  itg10a  24780  itg1ge0a  24781  itg1climres  24784  mbfi1fseqlem4  24788  ply1remlem  25232  ply1rem  25233  fta1glem1  25235  fta1glem2  25236  fta1g  25237  fta1blem  25238  plyco0  25258  ofmulrt  25347  plyremlem  25369  plyrem  25370  fta1lem  25372  fta1  25373  vieta1lem1  25375  vieta1lem2  25376  vieta1  25377  plyexmo  25378  elaa  25381  aannenlem1  25393  aalioulem2  25398  pilem1  25515  efif1olem3  25605  efif1olem4  25606  efifo  25608  eff1olem  25609  basellem4  26138  lgsqrlem2  26400  lgsqrlem3  26401  rpvmasum2  26565  dirith  26582  foresf1o  30751  ofpreima  30904  fnpreimac  30910  1stpreimas  30940  s3clhash  31124  pwrssmgc  31180  cycpmconjslem2  31324  cyc3conja  31326  dimkerim  31610  locfinreflem  31692  qqhre  31870  indpi1  31888  indpreima  31893  sibfof  32207  cvmliftlem6  33152  cvmliftlem7  33153  cvmliftlem8  33154  cvmliftlem9  33155  taupilem3  35417  itg2addnclem  35755  itg2addnclem2  35756  pw2f1o2val2  40778  dnnumch3  40788  proot1mul  40940  proot1hash  40941  proot1ex  40942  wessf1ornlem  42611  preimafvsnel  44719  uniimaprimaeqfv  44722  elsetpreimafvbi  44731