Theorem fniniseg 6880

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1543   ∈ wcel 2110  {csn 4541  ^◡ccnv 5550   “ cima 5554   Fn wfn 6375  ‘cfv 6380

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-br 5054  df-opab 5116  df-id 5455  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-iota 6338  df-fun 6382  df-fn 6383  df-fv 6388

This theorem is referenced by:  fparlem1  7880  fparlem2  7881  pw2f1olem  8749  recmulnq  10578  dmrecnq  10582  vdwlem1  16534  vdwlem2  16535  vdwlem6  16539  vdwlem8  16541  vdwlem9  16542  vdwlem12  16545  vdwlem13  16546  ramval  16561  ramub1lem1  16579  ghmeqker  18649  efgrelexlemb  19140  efgredeu  19142  psgnevpmb  20549  qtopeu  22613  itg1addlem1  24589  i1faddlem  24590  i1fmullem  24591  i1fmulclem  24600  i1fres  24603  itg10a  24608  itg1ge0a  24609  itg1climres  24612  mbfi1fseqlem4  24616  ply1remlem  25060  ply1rem  25061  fta1glem1  25063  fta1glem2  25064  fta1g  25065  fta1blem  25066  plyco0  25086  ofmulrt  25175  plyremlem  25197  plyrem  25198  fta1lem  25200  fta1  25201  vieta1lem1  25203  vieta1lem2  25204  vieta1  25205  plyexmo  25206  elaa  25209  aannenlem1  25221  aalioulem2  25226  pilem1  25343  efif1olem3  25433  efif1olem4  25434  efifo  25436  eff1olem  25437  basellem4  25966  lgsqrlem2  26228  lgsqrlem3  26229  rpvmasum2  26393  dirith  26410  foresf1o  30569  ofpreima  30722  fnpreimac  30728  1stpreimas  30758  s3clhash  30942  pwrssmgc  30997  cycpmconjslem2  31141  cyc3conja  31143  dimkerim  31422  locfinreflem  31504  qqhre  31682  indpi1  31700  indpreima  31705  sibfof  32019  cvmliftlem6  32965  cvmliftlem7  32966  cvmliftlem8  32967  cvmliftlem9  32968  taupilem3  35224  itg2addnclem  35565  itg2addnclem2  35566  pw2f1o2val2  40565  dnnumch3  40575  proot1mul  40727  proot1hash  40728  proot1ex  40729  wessf1ornlem  42395  preimafvsnel  44504  uniimaprimaeqfv  44507  elsetpreimafvbi  44516