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

Theorem fniniseg 5794
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 5793 . 2
2 fvex 5671 . . . 4
32elsnc 3878 . . 3
43anbi2i 679 . 2
51, 4syl6bb 255 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 178  /\wa 362  =wceq 1687  e.wcel 1749  {csn 3853  `'ccnv 4810  "cima 4814  Fnwfn 5385  `cfv 5390
This theorem is referenced by:  fparlem1  6641  fparlem2  6642  pw2f1olem  7374  recmulnq  9079  dmrecnq  9083  vdwlem1  13982  vdwlem2  13983  vdwlem6  13987  vdwlem8  13989  vdwlem9  13990  vdwlem12  13993  vdwlem13  13994  ramval  14009  ramub1lem1  14027  ghmeqker  15710  efgrelexlemb  16184  efgredeu  16186  psgnevpmb  17725  qtopeu  18993  itg1addlem1  20870  i1faddlem  20871  i1fmullem  20872  i1fmulclem  20880  i1fres  20883  itg10a  20888  itg1ge0a  20889  itg1climres  20892  mbfi1fseqlem4  20896  ply1remlem  21375  ply1rem  21376  fta1glem1  21378  fta1glem2  21379  fta1g  21380  fta1blem  21381  plyco0  21401  ofmulrt  21489  plyremlem  21511  plyrem  21512  fta1lem  21514  fta1  21515  vieta1lem1  21517  vieta1lem2  21518  vieta1  21519  plyexmo  21520  elaa  21523  aannenlem1  21535  aalioulem2  21540  pilem1  21657  efif1olem3  21741  efif1olem4  21742  efifo  21744  eff1olem  21745  basellem4  22162  lgsqrlem2  22422  lgsqrlem3  22423  rpvmasum2  22502  dirith  22519  ofpreima  25664  qqhre  26155  indpi1  26187  indpreima  26190  sibfof  26429  cvmliftlem6  26882  cvmliftlem7  26883  cvmliftlem8  26884  cvmliftlem9  26885  itg2addnclem  28114  itg2addnclem2  28115  pw2f1o2val2  29062  dnnumch3  29073  proot1mul  29237  proot1hash  29241  proot1ex  29242  taupilem3  35049
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-9 1753  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403  ax-sep 4388  ax-nul 4396  ax-pr 4503
This theorem depends on definitions:  df-bi 179  df-or 363  df-an 364  df-3an 952  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-eu 2248  df-mo 2249  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2547  df-ne 2587  df-ral 2699  df-rex 2700  df-rab 2703  df-v 2953  df-sbc 3165  df-dif 3308  df-un 3310  df-in 3312  df-ss 3319  df-nul 3615  df-if 3769  df-sn 3859  df-pr 3860  df-op 3862  df-uni 4067  df-br 4268  df-opab 4326  df-id 4607  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-iota 5353  df-fun 5392  df-fn 5393  df-fv 5398
  Copyright terms: Public domain W3C validator