Theorem elpreima 7030

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 6053	. . . . 5 ⊢ (◡𝐹 “ 𝐶) ⊆ dom 𝐹
2	1	sseli 3942	. . . 4 ⊢ (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ dom 𝐹)
3		fndm 6621	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2814	. . . 4 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴))
5	2, 4	imbitrid 244	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ 𝐴))
6		fnfun 6618	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
7		fvimacnvi 7024	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
8	6, 7	sylan 580	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
9	8	ex 412	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐹‘𝐵) ∈ 𝐶))
10	5, 9	jcad 512	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))
11		fvimacnv 7025	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
12	11	funfni 6624	. . . 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 2109  ^◡ccnv 5637  dom cdm 5638   “ cima 5641  Fun wfun 6505   Fn wfn 6506  ‘cfv 6511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-fv 6519

This theorem is referenced by:  elpreimad  7031  fniniseg  7032  fncnvima2  7033  unpreima  7035  respreima  7038  fnse  8112  brwitnlem  8471  unxpwdom2  9541  smobeth  10539  fpwwe2lem5  10588  hashkf  14297  isercolllem2  15632  isercolllem3  15633  isercoll  15634  fsumss  15691  fprodss  15914  tanval  16096  1arith  16898  0ram  16991  ghmpreima  19170  ghmnsgpreima  19173  kerf1ghm  19179  torsubg  19784  lmhmpreima  20955  rhmpreimaidl  21187  znunithash  21474  mpfind  22014  cncnpi  23165  cncnp  23167  cnpdis  23180  cnt0  23233  cnhaus  23241  2ndcomap  23345  1stccnp  23349  ptpjpre1  23458  tx1cn  23496  tx2cn  23497  txcnmpt  23511  txdis1cn  23522  hauseqlcld  23533  xkoptsub  23541  xkococn  23547  kqsat  23618  kqcldsat  23620  kqreglem1  23628  kqreglem2  23629  reghmph  23680  ordthmeolem  23688  tmdcn2  23976  clssubg  23996  tgphaus  24004  qustgplem  24008  ucncn  24172  xmeterval  24320  imasf1obl  24376  blval2  24450  metuel2  24453  isnghm  24611  cnbl0  24661  cnblcld  24662  cnheiborlem  24853  nmhmcn  25020  ismbl  25427  mbfeqalem1  25542  mbfmulc2lem  25548  mbfmax  25550  mbfposr  25553  mbfimaopnlem  25556  mbfaddlem  25561  mbfsup  25565  i1f1lem  25590  i1fpos  25607  mbfi1fseqlem4  25619  itg2monolem1  25651  itg2gt0  25661  itg2cnlem1  25662  itg2cnlem2  25663  plyeq0lem  26115  dgrlem  26134  dgrub  26139  dgrlb  26141  pserulm  26331  psercnlem2  26334  psercnlem1  26335  psercn  26336  abelth  26351  eff1olem  26457  ellogrn  26468  dvloglem  26557  logf1o2  26559  efopnlem1  26565  efopnlem2  26566  logtayl  26569  cxpcn3lem  26657  cxpcn3  26658  resqrtcn  26659  asinneg  26796  areambl  26868  sqff1o  27092  ubthlem1  30799  unipreima  32567  suppiniseg  32609  1stpreima  32630  2ndpreima  32631  suppss3  32647  hashgt1  32733  pwrssmgc  32926  tocyc01  33075  cyc3evpm  33107  elrgspnsubrunlem2  33199  kerunit  33297  elrspunidl  33399  rhmpreimaprmidl  33422  ply1degltel  33560  ply1degleel  33561  ply1degltdimlem  33618  irngnminplynz  33702  smatrcl  33786  rhmpreimacnlem  33874  cnre2csqlem  33900  elzrhunit  33967  qqhval2lem  33971  qqhf  33976  1stmbfm  34251  2ndmbfm  34252  mbfmcnt  34259  eulerpartlemsv2  34349  eulerpartlemv  34355  eulerpartlemf  34361  eulerpartlemgvv  34367  eulerpartlemgh  34369  eulerpartlemgs2  34371  sseqmw  34382  sseqf  34383  sseqp1  34386  fiblem  34389  fibp1  34392  cvmseu  35263  cvmliftmolem1  35268  cvmliftmolem2  35269  cvmliftlem15  35285  cvmlift2lem10  35299  cvmlift3lem8  35313  elmthm  35563  mthmblem  35567  mclsppslem  35570  mclspps  35571  cnambfre  37662  dvtan  37664  ftc1anclem3  37689  ftc1anclem5  37691  areacirc  37707  sstotbnd2  37768  keridl  38026  ellkr  39082  pw2f1ocnv  43026  binomcxplemdvbinom  44342  binomcxplemcvg  44343  binomcxplemnotnn0  44345  permaxpow  44999  rfcnpre1  45013  rfcnpre2  45025  rfcnpre3  45027  rfcnpre4  45028  limsupresxr  45764  liminfresxr  45765  icccncfext  45885  sge0fodjrnlem  46414  smfsuplem1  46809