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

Theorem elpreima 7006
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 6032 . . . . 5 (𝐹𝐶) ⊆ dom 𝐹
21sseli 3939 . . . 4 (𝐵 ∈ (𝐹𝐶) → 𝐵 ∈ dom 𝐹)
3 fndm 6603 . . . . 5 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
43eleq2d 2823 . . . 4 (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹𝐵𝐴))
52, 4imbitrid 243 . . 3 (𝐹 Fn 𝐴 → (𝐵 ∈ (𝐹𝐶) → 𝐵𝐴))
6 fnfun 6600 . . . . 5 (𝐹 Fn 𝐴 → Fun 𝐹)
7 fvimacnvi 7000 . . . . 5 ((Fun 𝐹𝐵 ∈ (𝐹𝐶)) → (𝐹𝐵) ∈ 𝐶)
86, 7sylan 580 . . . 4 ((𝐹 Fn 𝐴𝐵 ∈ (𝐹𝐶)) → (𝐹𝐵) ∈ 𝐶)
98ex 413 . . 3 (𝐹 Fn 𝐴 → (𝐵 ∈ (𝐹𝐶) → (𝐹𝐵) ∈ 𝐶))
105, 9jcad 513 . 2 (𝐹 Fn 𝐴 → (𝐵 ∈ (𝐹𝐶) → (𝐵𝐴 ∧ (𝐹𝐵) ∈ 𝐶)))
11 fvimacnv 7001 . . . . 5 ((Fun 𝐹𝐵 ∈ dom 𝐹) → ((𝐹𝐵) ∈ 𝐶𝐵 ∈ (𝐹𝐶)))
1211funfni 6606 . . . 4 ((𝐹 Fn 𝐴𝐵𝐴) → ((𝐹𝐵) ∈ 𝐶𝐵 ∈ (𝐹𝐶)))
1312biimpd 228 . . 3 ((𝐹 Fn 𝐴𝐵𝐴) → ((𝐹𝐵) ∈ 𝐶𝐵 ∈ (𝐹𝐶)))
1413expimpd 454 . 2 (𝐹 Fn 𝐴 → ((𝐵𝐴 ∧ (𝐹𝐵) ∈ 𝐶) → 𝐵 ∈ (𝐹𝐶)))
1510, 14impbid 211 1 (𝐹 Fn 𝐴 → (𝐵 ∈ (𝐹𝐶) ↔ (𝐵𝐴 ∧ (𝐹𝐵) ∈ 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wcel 2106  ccnv 5631  dom cdm 5632  cima 5635  Fun wfun 6488   Fn wfn 6489  cfv 6494
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2707  ax-sep 5255  ax-nul 5262  ax-pr 5383
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2943  df-ral 3064  df-rex 3073  df-rab 3407  df-v 3446  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-br 5105  df-opab 5167  df-id 5530  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6446  df-fun 6496  df-fn 6497  df-fv 6502
This theorem is referenced by:  elpreimad  7007  fniniseg  7008  fncnvima2  7009  unpreima  7011  respreima  7014  fnse  8062  brwitnlem  8450  unxpwdom2  9521  smobeth  10519  fpwwe2lem5  10568  hashkf  14229  isercolllem2  15547  isercolllem3  15548  isercoll  15549  fsumss  15607  fprodss  15828  tanval  16007  1arith  16796  0ram  16889  ghmpreima  19026  ghmnsgpreima  19029  torsubg  19628  kerf1ghm  20173  lmhmpreima  20505  znunithash  20967  mpfind  21513  cncnpi  22625  cncnp  22627  cnpdis  22640  cnt0  22693  cnhaus  22701  2ndcomap  22805  1stccnp  22809  ptpjpre1  22918  tx1cn  22956  tx2cn  22957  txcnmpt  22971  txdis1cn  22982  hauseqlcld  22993  xkoptsub  23001  xkococn  23007  kqsat  23078  kqcldsat  23080  kqreglem1  23088  kqreglem2  23089  reghmph  23140  ordthmeolem  23148  tmdcn2  23436  clssubg  23456  tgphaus  23464  qustgplem  23468  ucncn  23633  xmeterval  23781  imasf1obl  23840  blval2  23914  metuel2  23917  isnghm  24083  cnbl0  24133  cnblcld  24134  cnheiborlem  24313  nmhmcn  24479  ismbl  24886  mbfeqalem1  25001  mbfmulc2lem  25007  mbfmax  25009  mbfposr  25012  mbfimaopnlem  25015  mbfaddlem  25020  mbfsup  25024  i1f1lem  25049  i1fpos  25067  mbfi1fseqlem4  25079  itg2monolem1  25111  itg2gt0  25121  itg2cnlem1  25122  itg2cnlem2  25123  plyeq0lem  25567  dgrlem  25586  dgrub  25591  dgrlb  25593  pserulm  25777  psercnlem2  25779  psercnlem1  25780  psercn  25781  abelth  25796  eff1olem  25900  ellogrn  25911  dvloglem  25999  logf1o2  26001  efopnlem1  26007  efopnlem2  26008  logtayl  26011  cxpcn3lem  26096  cxpcn3  26097  resqrtcn  26098  asinneg  26232  areambl  26304  sqff1o  26527  ubthlem1  29710  unipreima  31458  suppiniseg  31497  1stpreima  31516  2ndpreima  31517  suppss3  31536  hashgt1  31605  pwrssmgc  31755  tocyc01  31862  cyc3evpm  31894  kerunit  32009  rhmpreimaidl  32091  elrspunidl  32094  rhmpreimaprmidl  32115  smatrcl  32268  rhmpreimacnlem  32356  cnre2csqlem  32382  elzrhunit  32451  qqhval2lem  32453  qqhf  32458  1stmbfm  32751  2ndmbfm  32752  mbfmcnt  32759  eulerpartlemsv2  32849  eulerpartlemv  32855  eulerpartlemf  32861  eulerpartlemgvv  32867  eulerpartlemgh  32869  eulerpartlemgs2  32871  sseqmw  32882  sseqf  32883  sseqp1  32886  fiblem  32889  fibp1  32892  cvmseu  33761  cvmliftmolem1  33766  cvmliftmolem2  33767  cvmliftlem15  33783  cvmlift2lem10  33797  cvmlift3lem8  33811  elmthm  34061  mthmblem  34065  mclsppslem  34068  mclspps  34069  cnambfre  36115  dvtan  36117  ftc1anclem3  36142  ftc1anclem5  36144  areacirc  36160  sstotbnd2  36222  keridl  36480  ellkr  37540  pw2f1ocnv  41337  binomcxplemdvbinom  42613  binomcxplemcvg  42614  binomcxplemnotnn0  42616  rfcnpre1  43204  rfcnpre2  43216  rfcnpre3  43218  rfcnpre4  43219  limsupresxr  43977  liminfresxr  43978  icccncfext  44098  sge0fodjrnlem  44627  smfsuplem1  45022
  Copyright terms: Public domain W3C validator