Theorem fniniseg 7014

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 7012	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵})))
2		fvex 6855	. . . 4 ⊢ (𝐹‘𝐶) ∈ V
3	2	elsn 4597	. . 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 4582  ^◡ccnv 5631   “ cima 5635   Fn wfn 6495  ‘cfv 6500

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 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-fv 6508

This theorem is referenced by:  fparlem1  8064  fparlem2  8065  pw2f1olem  9021  recmulnq  10887  dmrecnq  10891  vdwlem1  16921  vdwlem2  16922  vdwlem6  16926  vdwlem8  16928  vdwlem9  16929  vdwlem12  16932  vdwlem13  16933  ramval  16948  ramub1lem1  16966  ghmeqker  19184  ghmqusnsglem1  19221  ghmquskerlem1  19224  ghmqusker  19228  efgrelexlemb  19691  efgredeu  19693  psgnevpmb  21554  qtopeu  23672  itg1addlem1  25661  i1faddlem  25662  i1fmullem  25663  i1fmulclem  25671  i1fres  25674  itg10a  25679  itg1ge0a  25680  itg1climres  25683  mbfi1fseqlem4  25687  ply1remlem  26138  ply1rem  26139  fta1glem1  26141  fta1glem2  26142  fta1g  26143  fta1blem  26144  plyco0  26165  ofmulrt  26257  plyremlem  26280  plyrem  26281  fta1lem  26283  fta1  26284  vieta1lem1  26286  vieta1lem2  26287  vieta1  26288  plyexmo  26289  elaa  26292  aannenlem1  26304  aalioulem2  26309  pilem1  26429  efif1olem3  26521  efif1olem4  26522  efifo  26524  eff1olem  26525  basellem4  27062  lgsqrlem2  27326  lgsqrlem3  27327  rpvmasum2  27491  dirith  27508  foresf1o  32591  ofpreima  32755  fnpreimac  32760  1stpreimas  32796  indpi1  32952  indpreima  32958  s3clhash  33041  pwrssmgc  33093  cycpmconjslem2  33249  cyc3conja  33251  exsslsb  33774  dimkerim  33805  elirng  33864  irngss  33865  irngnzply1  33869  locfinreflem  34018  qqhre  34198  sibfof  34518  cvmliftlem6  35506  cvmliftlem7  35507  cvmliftlem8  35508  cvmliftlem9  35509  taupilem3  37574  itg2addnclem  37922  itg2addnclem2  37923  pw2f1o2val2  43397  dnnumch3  43404  proot1mul  43551  proot1hash  43552  proot1ex  43553  wessf1ornlem  45544  preimafvsnel  47739  uniimaprimaeqfv  47742  elsetpreimafvbi  47751  imasubc  49510  imassc  49512  imaid  49513