Theorem elpreima 7010

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 6047	. . . . 5 ⊢ (◡𝐹 “ 𝐶) ⊆ dom 𝐹
2	1	sseli 3917	. . . 4 ⊢ (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ dom 𝐹)
3		fndm 6601	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2822	. . . 4 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴))
5	2, 4	imbitrid 244	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ 𝐴))
6		fnfun 6598	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
7		fvimacnvi 7004	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
8	6, 7	sylan 581	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
9	8	ex 412	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐹‘𝐵) ∈ 𝐶))
10	5, 9	jcad 512	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))
11		fvimacnv 7005	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
12	11	funfni 6604	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
13	12	biimpd 229	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) ∈ 𝐶 → 𝐵 ∈ (◡𝐹 “ 𝐶)))
14	13	expimpd 453	. 2 ⊢ (𝐹 Fn 𝐴 → ((𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶) → 𝐵 ∈ (◡𝐹 “ 𝐶)))
15	10, 14	impbid 212	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) ↔ (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2114  ^◡ccnv 5630  dom cdm 5631   “ cima 5634  Fun wfun 6492   Fn wfn 6493  ‘cfv 6498

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-fv 6506

This theorem is referenced by:  elpreimad  7011  fniniseg  7012  fncnvima2  7013  unpreima  7015  respreima  7018  fnse  8083  brwitnlem  8442  unxpwdom2  9503  smobeth  10509  fpwwe2lem5  10558  hashkf  14294  isercolllem2  15628  isercolllem3  15629  isercoll  15630  fsumss  15687  fprodss  15913  tanval  16095  1arith  16898  0ram  16991  ghmpreima  19213  ghmnsgpreima  19216  kerf1ghm  19222  torsubg  19829  lmhmpreima  21043  rhmpreimaidl  21275  znunithash  21544  mpfind  22093  cncnpi  23243  cncnp  23245  cnpdis  23258  cnt0  23311  cnhaus  23319  2ndcomap  23423  1stccnp  23427  ptpjpre1  23536  tx1cn  23574  tx2cn  23575  txcnmpt  23589  txdis1cn  23600  hauseqlcld  23611  xkoptsub  23619  xkococn  23625  kqsat  23696  kqcldsat  23698  kqreglem1  23706  kqreglem2  23707  reghmph  23758  ordthmeolem  23766  tmdcn2  24054  clssubg  24074  tgphaus  24082  qustgplem  24086  ucncn  24249  xmeterval  24397  imasf1obl  24453  blval2  24527  metuel2  24530  isnghm  24688  cnbl0  24738  cnblcld  24739  cnheiborlem  24921  nmhmcn  25087  ismbl  25493  mbfeqalem1  25608  mbfmulc2lem  25614  mbfmax  25616  mbfposr  25619  mbfimaopnlem  25622  mbfaddlem  25627  mbfsup  25631  i1f1lem  25656  i1fpos  25673  mbfi1fseqlem4  25685  itg2monolem1  25717  itg2gt0  25727  itg2cnlem1  25728  itg2cnlem2  25729  plyeq0lem  26175  dgrlem  26194  dgrub  26199  dgrlb  26201  pserulm  26387  psercnlem2  26389  psercnlem1  26390  psercn  26391  abelth  26406  eff1olem  26512  ellogrn  26523  dvloglem  26612  logf1o2  26614  efopnlem1  26620  efopnlem2  26621  logtayl  26624  cxpcn3lem  26711  cxpcn3  26712  resqrtcn  26713  asinneg  26850  areambl  26922  sqff1o  27145  ubthlem1  30941  unipreima  32716  suppiniseg  32759  1stpreima  32780  2ndpreima  32781  suppss3  32796  hashgt1  32881  pwrssmgc  33060  tocyc01  33179  cyc3evpm  33211  elrgspnsubrunlem2  33309  kerunit  33385  elrspunidl  33488  rhmpreimaprmidl  33511  ply1degltel  33654  ply1degleel  33655  ply1degltdimlem  33766  irngnminplynz  33856  smatrcl  33940  rhmpreimacnlem  34028  cnre2csqlem  34054  elzrhunit  34121  qqhval2lem  34125  qqhf  34130  1stmbfm  34404  2ndmbfm  34405  mbfmcnt  34412  eulerpartlemsv2  34502  eulerpartlemv  34508  eulerpartlemf  34514  eulerpartlemgvv  34520  eulerpartlemgh  34522  eulerpartlemgs2  34524  sseqmw  34535  sseqf  34536  sseqp1  34539  fiblem  34542  fibp1  34545  cvmseu  35458  cvmliftmolem1  35463  cvmliftmolem2  35464  cvmliftlem15  35480  cvmlift2lem10  35494  cvmlift3lem8  35508  elmthm  35758  mthmblem  35762  mclsppslem  35765  mclspps  35766  cnambfre  37989  dvtan  37991  ftc1anclem3  38016  ftc1anclem5  38018  areacirc  38034  sstotbnd2  38095  keridl  38353  ellkr  39535  pw2f1ocnv  43465  binomcxplemdvbinom  44780  binomcxplemcvg  44781  binomcxplemnotnn0  44783  permaxpow  45436  rfcnpre1  45450  rfcnpre2  45462  rfcnpre3  45464  rfcnpre4  45465  limsupresxr  46194  liminfresxr  46195  icccncfext  46315  sge0fodjrnlem  46844  smfsuplem1  47239