Theorem elpreima 7054

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

Step	Hyp	Ref	Expression
1		cnvimass 6082	. . . . 5 ⊢ (◡𝐹 “ 𝐶) ⊆ dom 𝐹
2	1	sseli 3930	. . . 4 ⊢ (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ dom 𝐹)
3		fndm 6639	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2848	. . . 4 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴))
5	2, 4	imbitrid 247	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ 𝐴))
6		fnfun 6636	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
7		fvimacnvi 7048	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
8	6, 7	sylan 592	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
9	8	ex 418	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐹‘𝐵) ∈ 𝐶))
10	5, 9	jcad 522	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))
11		fvimacnv 7049	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
12	11	funfni 6642	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
13	12	biimpd 232	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) ∈ 𝐶 → 𝐵 ∈ (◡𝐹 “ 𝐶)))
14	13	expimpd 459	. 2 ⊢ (𝐹 Fn 𝐴 → ((𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶) → 𝐵 ∈ (◡𝐹 “ 𝐶)))
15	10, 14	impbid 215	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) ↔ (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2145  ^◡ccnv 5658  dom cdm 5659   “ cima 5662  Fun wfun 6531   Fn wfn 6532  ‘cfv 6537

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-fv 6545

This theorem is used by:  elpreimad  7055  fniniseg  7056  fncnvima2  7057  unpreima  7059  respreima  7062  fnse  8135  brwitnlem  8498  unxpwdom2  9564  smobeth  10599  fpwwe2lem5  10648  hashkf  14400  isercolllem2  15757  isercolllem3  15758  isercoll  15759  fsumss  15815  fprodss  16041  tanval  16222  1arith  17025  0ram  17118  ghmpreima  19371  ghmnsgpreima  19374  kerf1ghm  19380  torsubg  19987  lmhmpreima  21238  rhmpreimaidl  21485  rhmpreimaprmidl  21548  znunithash  21783  mpfind  22337  cncnpi  23509  cncnp  23511  cnpdis  23524  cnt0  23577  cnhaus  23585  2ndcomap  23690  1stccnp  23694  ptpjpre1  23803  tx1cn  23841  tx2cn  23842  txcnmpt  23856  txdis1cn  23867  hauseqlcld  23878  xkoptsub  23886  xkococn  23892  kqsat  23963  kqcldsat  23965  kqreglem1  23973  kqreglem2  23974  reghmph  24025  ordthmeolem  24033  tmdcn2  24321  clssubg  24341  tgphaus  24349  qustgplem  24353  ucncn  24516  xmeterval  24664  imasf1obl  24720  blval2  24794  metuel2  24797  isnghm  24955  cnbl0  25005  cnblcld  25006  cnheiborlem  25188  nmhmcn  25354  ismbl  25760  mbfeqalem1  25875  mbfmulc2lem  25881  mbfmax  25883  mbfposr  25886  mbfimaopnlem  25889  mbfaddlem  25894  mbfsup  25898  i1f1lem  25923  i1fpos  25940  mbfi1fseqlem4  25952  itg2monolem1  25984  itg2gt0  25994  itg2cnlem1  25995  itg2cnlem2  25996  plyeq0lem  26443  dgrlem  26462  dgrub  26467  dgrlb  26469  pserulm  26665  psercnlem2  26667  psercnlem1  26668  psercn  26669  abelth  26684  eff1olem  26793  ellogrn  26804  dvloglem  26893  logf1o2  26895  efopnlem1  26901  efopnlem2  26902  logtayl  26905  cxpcn3lem  26992  cxpcn3  26993  resqrtcn  26994  asinneg  27131  areambl  27203  sqff1o  27426  ubthlem1  31359  unipreima  33124  suppiniseg  33166  1stpreima  33187  2ndpreima  33188  suppss3  33202  hashgt1  33287  pwrssmgc  33448  tocyc01  33566  cyc3evpm  33598  elrgspnsubrunlem2  33696  kerunit  33773  elrspunidl  33864  ply1degltel  34012  ply1degleel  34013  ply1degltdimlem  34140  irngnminplynz  34230  smatrcl  34314  rhmpreimacnlem  34402  cnre2csqlem  34428  elzrhunit  34495  qqhval2lem  34499  qqhf  34504  1stmbfm  34779  2ndmbfm  34780  mbfmcnt  34787  eulerpartlemsv2  34877  eulerpartlemv  34883  eulerpartlemf  34889  eulerpartlemgvv  34895  eulerpartlemgh  34897  eulerpartlemgs2  34899  sseqmw  34910  sseqf  34911  sseqp1  34914  fiblem  34917  fibp1  34920  cvmseu  35863  cvmliftmolem1  35868  cvmliftmolem2  35869  cvmliftlem15  35885  cvmlift2lem10  35899  cvmlift3lem8  35913  elmthm  36163  mthmblem  36167  mclsppslem  36170  mclspps  36171  cnambfre  38425  dvtan  38427  ftc1anclem3  38452  ftc1anclem5  38454  areacirc  38470  sstotbnd2  38532  keridl  38790  ellkr  39970  pw2f1ocnv  43886  binomcxplemdvbinom  45185  binomcxplemcvg  45186  binomcxplemnotnn0  45188  permaxpow  45840  rfcnpre1  45861  rfcnpre2  45873  rfcnpre3  45875  rfcnpre4  45876  limsupresxr  46602  liminfresxr  46603  icccncfext  46723  sge0fodjrnlem  47252  smfsuplem1  47647