Theorem fniniseg 7006

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 7004	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵})))
2		fvex 6847	. . . 4 ⊢ (𝐹‘𝐶) ∈ V
3	2	elsn 4583	. . 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 4568  ^◡ccnv 5623   “ cima 5627   Fn wfn 6487  ‘cfv 6492

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 5231  ax-nul 5241  ax-pr 5370

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-fv 6500

This theorem is referenced by:  fparlem1  8055  fparlem2  8056  pw2f1olem  9012  recmulnq  10878  dmrecnq  10882  indpi1  12164  vdwlem1  16943  vdwlem2  16944  vdwlem6  16948  vdwlem8  16950  vdwlem9  16951  vdwlem12  16954  vdwlem13  16955  ramval  16970  ramub1lem1  16988  ghmeqker  19209  ghmqusnsglem1  19246  ghmquskerlem1  19249  ghmqusker  19253  efgrelexlemb  19716  efgredeu  19718  psgnevpmb  21577  qtopeu  23691  itg1addlem1  25669  i1faddlem  25670  i1fmullem  25671  i1fmulclem  25679  i1fres  25682  itg10a  25687  itg1ge0a  25688  itg1climres  25691  mbfi1fseqlem4  25695  ply1remlem  26140  ply1rem  26141  fta1glem1  26143  fta1glem2  26144  fta1g  26145  fta1blem  26146  plyco0  26167  ofmulrt  26258  plyremlem  26281  plyrem  26282  fta1lem  26284  fta1  26285  vieta1lem1  26287  vieta1lem2  26288  vieta1  26289  plyexmo  26290  elaa  26293  aannenlem1  26305  aalioulem2  26310  pilem1  26429  efif1olem3  26521  efif1olem4  26522  efifo  26524  eff1olem  26525  basellem4  27061  lgsqrlem2  27324  lgsqrlem3  27325  rpvmasum2  27489  dirith  27506  foresf1o  32589  ofpreima  32753  fnpreimac  32758  1stpreimas  32794  indpreima  32940  s3clhash  33023  pwrssmgc  33075  cycpmconjslem2  33231  cyc3conja  33233  exsslsb  33756  dimkerim  33787  elirng  33846  irngss  33847  irngnzply1  33851  locfinreflem  34000  qqhre  34180  sibfof  34500  cvmliftlem6  35488  cvmliftlem7  35489  cvmliftlem8  35490  cvmliftlem9  35491  taupilem3  37649  itg2addnclem  38006  itg2addnclem2  38007  pw2f1o2val2  43486  dnnumch3  43493  proot1mul  43640  proot1hash  43641  proot1ex  43642  wessf1ornlem  45633  preimafvsnel  47851  uniimaprimaeqfv  47854  elsetpreimafvbi  47863  imasubc  49638  imassc  49640  imaid  49641