MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elpreima Structured version   Visualization version   GIF version

Theorem elpreima 7009
Description: Membership in the preimage of a set under a function. (Contributed by Jeff Madsen, 2-Sep-2009.)
Assertion
Ref Expression
elpreima (𝐹 Fn 𝐴 → (𝐵 ∈ (𝐹𝐶) ↔ (𝐵𝐴 ∧ (𝐹𝐵) ∈ 𝐶)))

Proof of Theorem elpreima
StepHypRef Expression
1 cnvimass 6034 . . . . 5 (𝐹𝐶) ⊆ dom 𝐹
21sseli 3941 . . . 4 (𝐵 ∈ (𝐹𝐶) → 𝐵 ∈ dom 𝐹)
3 fndm 6606 . . . . 5 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
43eleq2d 2824 . . . 4 (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹𝐵𝐴))
52, 4imbitrid 243 . . 3 (𝐹 Fn 𝐴 → (𝐵 ∈ (𝐹𝐶) → 𝐵𝐴))
6 fnfun 6603 . . . . 5 (𝐹 Fn 𝐴 → Fun 𝐹)
7 fvimacnvi 7003 . . . . 5 ((Fun 𝐹𝐵 ∈ (𝐹𝐶)) → (𝐹𝐵) ∈ 𝐶)
86, 7sylan 581 . . . 4 ((𝐹 Fn 𝐴𝐵 ∈ (𝐹𝐶)) → (𝐹𝐵) ∈ 𝐶)
98ex 414 . . 3 (𝐹 Fn 𝐴 → (𝐵 ∈ (𝐹𝐶) → (𝐹𝐵) ∈ 𝐶))
105, 9jcad 514 . 2 (𝐹 Fn 𝐴 → (𝐵 ∈ (𝐹𝐶) → (𝐵𝐴 ∧ (𝐹𝐵) ∈ 𝐶)))
11 fvimacnv 7004 . . . . 5 ((Fun 𝐹𝐵 ∈ dom 𝐹) → ((𝐹𝐵) ∈ 𝐶𝐵 ∈ (𝐹𝐶)))
1211funfni 6609 . . . 4 ((𝐹 Fn 𝐴𝐵𝐴) → ((𝐹𝐵) ∈ 𝐶𝐵 ∈ (𝐹𝐶)))
1312biimpd 228 . . 3 ((𝐹 Fn 𝐴𝐵𝐴) → ((𝐹𝐵) ∈ 𝐶𝐵 ∈ (𝐹𝐶)))
1413expimpd 455 . 2 (𝐹 Fn 𝐴 → ((𝐵𝐴 ∧ (𝐹𝐵) ∈ 𝐶) → 𝐵 ∈ (𝐹𝐶)))
1510, 14impbid 211 1 (𝐹 Fn 𝐴 → (𝐵 ∈ (𝐹𝐶) ↔ (𝐵𝐴 ∧ (𝐹𝐵) ∈ 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  wcel 2107  ccnv 5633  dom cdm 5634  cima 5637  Fun wfun 6491   Fn wfn 6492  cfv 6497
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pr 5385
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2945  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-fv 6505
This theorem is referenced by:  elpreimad  7010  fniniseg  7011  fncnvima2  7012  unpreima  7014  respreima  7017  fnse  8066  brwitnlem  8454  unxpwdom2  9525  smobeth  10523  fpwwe2lem5  10572  hashkf  14233  isercolllem2  15551  isercolllem3  15552  isercoll  15553  fsumss  15611  fprodss  15832  tanval  16011  1arith  16800  0ram  16893  ghmpreima  19031  ghmnsgpreima  19034  torsubg  19633  kerf1ghm  20178  lmhmpreima  20512  znunithash  20974  mpfind  21520  cncnpi  22632  cncnp  22634  cnpdis  22647  cnt0  22700  cnhaus  22708  2ndcomap  22812  1stccnp  22816  ptpjpre1  22925  tx1cn  22963  tx2cn  22964  txcnmpt  22978  txdis1cn  22989  hauseqlcld  23000  xkoptsub  23008  xkococn  23014  kqsat  23085  kqcldsat  23087  kqreglem1  23095  kqreglem2  23096  reghmph  23147  ordthmeolem  23155  tmdcn2  23443  clssubg  23463  tgphaus  23471  qustgplem  23475  ucncn  23640  xmeterval  23788  imasf1obl  23847  blval2  23921  metuel2  23924  isnghm  24090  cnbl0  24140  cnblcld  24141  cnheiborlem  24320  nmhmcn  24486  ismbl  24893  mbfeqalem1  25008  mbfmulc2lem  25014  mbfmax  25016  mbfposr  25019  mbfimaopnlem  25022  mbfaddlem  25027  mbfsup  25031  i1f1lem  25056  i1fpos  25074  mbfi1fseqlem4  25086  itg2monolem1  25118  itg2gt0  25128  itg2cnlem1  25129  itg2cnlem2  25130  plyeq0lem  25574  dgrlem  25593  dgrub  25598  dgrlb  25600  pserulm  25784  psercnlem2  25786  psercnlem1  25787  psercn  25788  abelth  25803  eff1olem  25907  ellogrn  25918  dvloglem  26006  logf1o2  26008  efopnlem1  26014  efopnlem2  26015  logtayl  26018  cxpcn3lem  26103  cxpcn3  26104  resqrtcn  26105  asinneg  26239  areambl  26311  sqff1o  26534  ubthlem1  29815  unipreima  31563  suppiniseg  31604  1stpreima  31623  2ndpreima  31624  suppss3  31644  hashgt1  31713  pwrssmgc  31863  tocyc01  31970  cyc3evpm  32002  kerunit  32117  rhmpreimaidl  32203  elrspunidl  32206  rhmpreimaprmidl  32227  smatrcl  32380  rhmpreimacnlem  32468  cnre2csqlem  32494  elzrhunit  32563  qqhval2lem  32565  qqhf  32570  1stmbfm  32863  2ndmbfm  32864  mbfmcnt  32871  eulerpartlemsv2  32961  eulerpartlemv  32967  eulerpartlemf  32973  eulerpartlemgvv  32979  eulerpartlemgh  32981  eulerpartlemgs2  32983  sseqmw  32994  sseqf  32995  sseqp1  32998  fiblem  33001  fibp1  33004  cvmseu  33873  cvmliftmolem1  33878  cvmliftmolem2  33879  cvmliftlem15  33895  cvmlift2lem10  33909  cvmlift3lem8  33923  elmthm  34173  mthmblem  34177  mclsppslem  34180  mclspps  34181  cnambfre  36129  dvtan  36131  ftc1anclem3  36156  ftc1anclem5  36158  areacirc  36174  sstotbnd2  36236  keridl  36494  ellkr  37554  pw2f1ocnv  41364  binomcxplemdvbinom  42640  binomcxplemcvg  42641  binomcxplemnotnn0  42643  rfcnpre1  43231  rfcnpre2  43243  rfcnpre3  43245  rfcnpre4  43246  limsupresxr  44014  liminfresxr  44015  icccncfext  44135  sge0fodjrnlem  44664  smfsuplem1  45059
  Copyright terms: Public domain W3C validator