MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fniniseg Unicode version

Theorem fniniseg 5947
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

Proof of Theorem fniniseg
StepHypRef Expression
1 elpreima 5946 . 2
2 fvex 5823 . . . 4
32elsnc 4017 . . 3
43anbi2i 694 . 2
51, 4syl6bb 261 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1370  e.wcel 1758  {csn 3993  `'ccnv 4956  "cima 4960  Fnwfn 5532  `cfv 5537
This theorem is referenced by:  fparlem1  6806  fparlem2  6807  pw2f1olem  7549  recmulnq  9270  dmrecnq  9274  vdwlem1  14200  vdwlem2  14201  vdwlem6  14205  vdwlem8  14207  vdwlem9  14208  vdwlem12  14211  vdwlem13  14212  ramval  14227  ramub1lem1  14245  ghmeqker  15932  efgrelexlemb  16408  efgredeu  16410  psgnevpmb  18210  qtopeu  19688  itg1addlem1  21570  i1faddlem  21571  i1fmullem  21572  i1fmulclem  21580  i1fres  21583  itg10a  21588  itg1ge0a  21589  itg1climres  21592  mbfi1fseqlem4  21596  ply1remlem  22034  ply1rem  22035  fta1glem1  22037  fta1glem2  22038  fta1g  22039  fta1blem  22040  plyco0  22060  ofmulrt  22148  plyremlem  22170  plyrem  22171  fta1lem  22173  fta1  22174  vieta1lem1  22176  vieta1lem2  22177  vieta1  22178  plyexmo  22179  elaa  22182  aannenlem1  22194  aalioulem2  22199  pilem1  22316  efif1olem3  22400  efif1olem4  22401  efifo  22403  eff1olem  22404  basellem4  22821  lgsqrlem2  23081  lgsqrlem3  23082  rpvmasum2  23161  dirith  23178  ofpreima  26451  qqhre  26903  indpi1  26935  indpreima  26938  sibfof  27182  cvmliftlem6  27635  cvmliftlem7  27636  cvmliftlem8  27637  cvmliftlem9  27638  itg2addnclem  28903  itg2addnclem2  28904  pw2f1o2val2  29849  dnnumch3  29860  proot1mul  30024  proot1hash  30028  proot1ex  30029  taupilem3  36463
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4530  ax-nul 4538  ax-pr 4648
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2805  df-rex 2806  df-rab 2809  df-v 3083  df-sbc 3298  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3752  df-if 3906  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4209  df-br 4410  df-opab 4468  df-id 4753  df-xp 4963  df-rel 4964  df-cnv 4965  df-co 4966  df-dm 4967  df-rn 4968  df-res 4969  df-ima 4970  df-iota 5500  df-fun 5539  df-fn 5540  df-fv 5545
  Copyright terms: Public domain W3C validator