Theorem elpreima 6991

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 6030	. . . . 5 ⊢ (◡𝐹 “ 𝐶) ⊆ dom 𝐹
2	1	sseli 3925	. . . 4 ⊢ (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ dom 𝐹)
3		fndm 6584	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2817	. . . 4 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴))
5	2, 4	imbitrid 244	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ 𝐴))
6		fnfun 6581	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
7		fvimacnvi 6985	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
8	6, 7	sylan 580	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
9	8	ex 412	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐹‘𝐵) ∈ 𝐶))
10	5, 9	jcad 512	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))
11		fvimacnv 6986	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
12	11	funfni 6587	. . . 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 2111  ^◡ccnv 5613  dom cdm 5614   “ cima 5617  Fun wfun 6475   Fn wfn 6476  ‘cfv 6481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6437  df-fun 6483  df-fn 6484  df-fv 6489

This theorem is referenced by:  elpreimad  6992  fniniseg  6993  fncnvima2  6994  unpreima  6996  respreima  6999  fnse  8063  brwitnlem  8422  unxpwdom2  9474  smobeth  10477  fpwwe2lem5  10526  hashkf  14239  isercolllem2  15573  isercolllem3  15574  isercoll  15575  fsumss  15632  fprodss  15855  tanval  16037  1arith  16839  0ram  16932  ghmpreima  19150  ghmnsgpreima  19153  kerf1ghm  19159  torsubg  19766  lmhmpreima  20982  rhmpreimaidl  21214  znunithash  21501  mpfind  22042  cncnpi  23193  cncnp  23195  cnpdis  23208  cnt0  23261  cnhaus  23269  2ndcomap  23373  1stccnp  23377  ptpjpre1  23486  tx1cn  23524  tx2cn  23525  txcnmpt  23539  txdis1cn  23550  hauseqlcld  23561  xkoptsub  23569  xkococn  23575  kqsat  23646  kqcldsat  23648  kqreglem1  23656  kqreglem2  23657  reghmph  23708  ordthmeolem  23716  tmdcn2  24004  clssubg  24024  tgphaus  24032  qustgplem  24036  ucncn  24199  xmeterval  24347  imasf1obl  24403  blval2  24477  metuel2  24480  isnghm  24638  cnbl0  24688  cnblcld  24689  cnheiborlem  24880  nmhmcn  25047  ismbl  25454  mbfeqalem1  25569  mbfmulc2lem  25575  mbfmax  25577  mbfposr  25580  mbfimaopnlem  25583  mbfaddlem  25588  mbfsup  25592  i1f1lem  25617  i1fpos  25634  mbfi1fseqlem4  25646  itg2monolem1  25678  itg2gt0  25688  itg2cnlem1  25689  itg2cnlem2  25690  plyeq0lem  26142  dgrlem  26161  dgrub  26166  dgrlb  26168  pserulm  26358  psercnlem2  26361  psercnlem1  26362  psercn  26363  abelth  26378  eff1olem  26484  ellogrn  26495  dvloglem  26584  logf1o2  26586  efopnlem1  26592  efopnlem2  26593  logtayl  26596  cxpcn3lem  26684  cxpcn3  26685  resqrtcn  26686  asinneg  26823  areambl  26895  sqff1o  27119  ubthlem1  30850  unipreima  32625  suppiniseg  32667  1stpreima  32688  2ndpreima  32689  suppss3  32706  hashgt1  32790  pwrssmgc  32981  tocyc01  33087  cyc3evpm  33119  elrgspnsubrunlem2  33215  kerunit  33290  elrspunidl  33393  rhmpreimaprmidl  33416  ply1degltel  33555  ply1degleel  33556  ply1degltdimlem  33635  irngnminplynz  33725  smatrcl  33809  rhmpreimacnlem  33897  cnre2csqlem  33923  elzrhunit  33990  qqhval2lem  33994  qqhf  33999  1stmbfm  34273  2ndmbfm  34274  mbfmcnt  34281  eulerpartlemsv2  34371  eulerpartlemv  34377  eulerpartlemf  34383  eulerpartlemgvv  34389  eulerpartlemgh  34391  eulerpartlemgs2  34393  sseqmw  34404  sseqf  34405  sseqp1  34408  fiblem  34411  fibp1  34414  cvmseu  35320  cvmliftmolem1  35325  cvmliftmolem2  35326  cvmliftlem15  35342  cvmlift2lem10  35356  cvmlift3lem8  35370  elmthm  35620  mthmblem  35624  mclsppslem  35627  mclspps  35628  cnambfre  37707  dvtan  37709  ftc1anclem3  37734  ftc1anclem5  37736  areacirc  37752  sstotbnd2  37813  keridl  38071  ellkr  39187  pw2f1ocnv  43129  binomcxplemdvbinom  44445  binomcxplemcvg  44446  binomcxplemnotnn0  44448  permaxpow  45101  rfcnpre1  45115  rfcnpre2  45127  rfcnpre3  45129  rfcnpre4  45130  limsupresxr  45863  liminfresxr  45864  icccncfext  45984  sge0fodjrnlem  46513  smfsuplem1  46908