Theorem fniniseg 7001

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 6999	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵})))
2		fvex 6840	. . . 4 ⊢ (𝐹‘𝐶) ∈ V
3	2	elsn 4570	. . 3 ⊢ ((𝐹‘𝐶) ∈ {𝐵} ↔ (𝐹‘𝐶) = 𝐵)
4	3	anbi2i 629	. 2 ⊢ ((𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵))
5	1, 4	bitrdi 288	1 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵)))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547   ∈ wcel 2119  {csn 4555  ^◡ccnv 5617   “ cima 5621   Fn wfn 6480  ‘cfv 6485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-fv 6493

This theorem is referenced by:  fparlem1  8051  fparlem2  8052  pw2f1olem  9009  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  21562  qtopeu  23699  itg1addlem1  25677  i1faddlem  25678  i1fmullem  25679  i1fmulclem  25687  i1fres  25690  itg10a  25695  itg1ge0a  25696  itg1climres  25699  mbfi1fseqlem4  25703  ply1remlem  26148  ply1rem  26149  fta1glem1  26151  fta1glem2  26152  fta1g  26153  fta1blem  26154  plyco0  26175  ofmulrt  26266  plyremlem  26288  plyrem  26289  fta1lem  26291  fta1  26292  vieta1lem1  26294  vieta1lem2  26295  vieta1  26296  plyexmo  26297  elaa  26300  aannenlem1  26312  aalioulem2  26317  pilem1  26434  efif1olem3  26526  efif1olem4  26527  efifo  26529  eff1olem  26530  basellem4  27065  lgsqrlem2  27328  lgsqrlem3  27329  rpvmasum2  27493  dirith  27510  foresf1o  32592  ofpreima  32757  fnpreimac  32762  1stpreimas  32798  indpreima  32944  s3clhash  33027  pwrssmgc  33079  cycpmconjslem2  33236  cyc3conja  33238  exsslsb  33781  dimkerim  33811  elirng  33870  irngss  33871  irngnzply1  33875  locfinreflem  34024  qqhre  34204  sibfof  34524  cvmliftlem6  35518  cvmliftlem7  35519  cvmliftlem8  35520  cvmliftlem9  35521  taupilem3  37679  itg2addnclem  38038  itg2addnclem2  38039  pw2f1o2val2  43485  dnnumch3  43492  proot1mul  43639  proot1hash  43640  proot1ex  43641  wessf1ornlem  45632  preimafvsnel  47854  uniimaprimaeqfv  47857  elsetpreimafvbi  47866  imasubc  49641  imassc  49643  imaid  49644