Theorem fniniseg 7007

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 7005	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵})))
2		fvex 6848	. . . 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 5624   “ cima 5628   Fn wfn 6488  ‘cfv 6493

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 5232  ax-nul 5242  ax-pr 5371

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 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-fv 6501

This theorem is referenced by:  fparlem1  8056  fparlem2  8057  pw2f1olem  9013  recmulnq  10881  dmrecnq  10885  indpi1  12167  vdwlem1  16946  vdwlem2  16947  vdwlem6  16951  vdwlem8  16953  vdwlem9  16954  vdwlem12  16957  vdwlem13  16958  ramval  16973  ramub1lem1  16991  ghmeqker  19212  ghmqusnsglem1  19249  ghmquskerlem1  19252  ghmqusker  19256  efgrelexlemb  19719  efgredeu  19721  psgnevpmb  21580  qtopeu  23694  itg1addlem1  25672  i1faddlem  25673  i1fmullem  25674  i1fmulclem  25682  i1fres  25685  itg10a  25690  itg1ge0a  25691  itg1climres  25694  mbfi1fseqlem4  25698  ply1remlem  26143  ply1rem  26144  fta1glem1  26146  fta1glem2  26147  fta1g  26148  fta1blem  26149  plyco0  26170  ofmulrt  26261  plyremlem  26284  plyrem  26285  fta1lem  26287  fta1  26288  vieta1lem1  26290  vieta1lem2  26291  vieta1  26292  plyexmo  26293  elaa  26296  aannenlem1  26308  aalioulem2  26313  pilem1  26432  efif1olem3  26524  efif1olem4  26525  efifo  26527  eff1olem  26528  basellem4  27064  lgsqrlem2  27327  lgsqrlem3  27328  rpvmasum2  27492  dirith  27509  foresf1o  32592  ofpreima  32756  fnpreimac  32761  1stpreimas  32797  indpreima  32943  s3clhash  33026  pwrssmgc  33078  cycpmconjslem2  33234  cyc3conja  33236  exsslsb  33759  dimkerim  33790  elirng  33849  irngss  33850  irngnzply1  33854  locfinreflem  34003  qqhre  34183  sibfof  34503  cvmliftlem6  35491  cvmliftlem7  35492  cvmliftlem8  35493  cvmliftlem9  35494  taupilem3  37652  itg2addnclem  38009  itg2addnclem2  38010  pw2f1o2val2  43489  dnnumch3  43496  proot1mul  43643  proot1hash  43644  proot1ex  43645  wessf1ornlem  45636  preimafvsnel  47854  uniimaprimaeqfv  47857  elsetpreimafvbi  47866  imasubc  49641  imassc  49643  imaid  49644