Theorem elpreima 7043

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 6075	. . . . 5 ⊢ (◡𝐹 “ 𝐶) ⊆ dom 𝐹
2	1	sseli 3935	. . . 4 ⊢ (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ dom 𝐹)
3		fndm 6628	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2851	. . . 4 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴))
5	2, 4	imbitrid 247	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ 𝐴))
6		fnfun 6625	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
7		fvimacnvi 7037	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
8	6, 7	sylan 591	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
9	8	ex 417	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐹‘𝐵) ∈ 𝐶))
10	5, 9	jcad 521	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))
11		fvimacnv 7038	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
12	11	funfni 6631	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
13	12	biimpd 232	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) ∈ 𝐶 → 𝐵 ∈ (◡𝐹 “ 𝐶)))
14	13	expimpd 458	. 2 ⊢ (𝐹 Fn 𝐴 → ((𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶) → 𝐵 ∈ (◡𝐹 “ 𝐶)))
15	10, 14	impbid 215	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) ↔ (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∈ wcel 2145  ^◡ccnv 5651  dom cdm 5652   “ cima 5655  Fun wfun 6519   Fn wfn 6520  ‘cfv 6525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-opab 5168  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-iota 6481  df-fun 6527  df-fn 6528  df-fv 6533

This theorem is referenced by:  elpreimad  7044  fniniseg  7045  fncnvima2  7046  unpreima  7048  respreima  7051  fnse  8117  brwitnlem  8480  unxpwdom2  9538  smobeth  10559  fpwwe2lem5  10608  hashkf  14359  isercolllem2  15707  isercolllem3  15708  isercoll  15709  fsumss  15766  fprodss  15992  tanval  16174  1arith  16977  0ram  17070  ghmpreima  19299  ghmnsgpreima  19302  kerf1ghm  19308  torsubg  19915  lmhmpreima  21138  rhmpreimaidl  21378  rhmpreimaprmidl  21439  znunithash  21674  mpfind  22226  cncnpi  23396  cncnp  23398  cnpdis  23411  cnt0  23464  cnhaus  23472  2ndcomap  23576  1stccnp  23580  ptpjpre1  23689  tx1cn  23727  tx2cn  23728  txcnmpt  23742  txdis1cn  23753  hauseqlcld  23764  xkoptsub  23772  xkococn  23778  kqsat  23849  kqcldsat  23851  kqreglem1  23859  kqreglem2  23860  reghmph  23911  ordthmeolem  23919  tmdcn2  24207  clssubg  24227  tgphaus  24235  qustgplem  24239  ucncn  24402  xmeterval  24550  imasf1obl  24606  blval2  24680  metuel2  24683  isnghm  24841  cnbl0  24891  cnblcld  24892  cnheiborlem  25074  nmhmcn  25240  ismbl  25646  mbfeqalem1  25761  mbfmulc2lem  25767  mbfmax  25769  mbfposr  25772  mbfimaopnlem  25775  mbfaddlem  25780  mbfsup  25784  i1f1lem  25809  i1fpos  25826  mbfi1fseqlem4  25838  itg2monolem1  25870  itg2gt0  25880  itg2cnlem1  25881  itg2cnlem2  25882  plyeq0lem  26328  dgrlem  26347  dgrub  26352  dgrlb  26354  pserulm  26543  psercnlem2  26545  psercnlem1  26546  psercn  26547  abelth  26562  eff1olem  26671  ellogrn  26682  dvloglem  26771  logf1o2  26773  efopnlem1  26779  efopnlem2  26780  logtayl  26783  cxpcn3lem  26870  cxpcn3  26871  resqrtcn  26872  asinneg  27009  areambl  27081  sqff1o  27304  ubthlem1  31131  unipreima  32900  suppiniseg  32943  1stpreima  32964  2ndpreima  32965  suppss3  32980  hashgt1  33065  pwrssmgc  33233  tocyc01  33351  cyc3evpm  33383  elrgspnsubrunlem2  33481  kerunit  33560  elrspunidl  33652  ply1degltel  33801  ply1degleel  33802  ply1degltdimlem  33929  irngnminplynz  34019  smatrcl  34103  rhmpreimacnlem  34191  cnre2csqlem  34217  elzrhunit  34284  qqhval2lem  34288  qqhf  34293  1stmbfm  34567  2ndmbfm  34568  mbfmcnt  34575  eulerpartlemsv2  34665  eulerpartlemv  34671  eulerpartlemf  34677  eulerpartlemgvv  34683  eulerpartlemgh  34685  eulerpartlemgs2  34687  sseqmw  34698  sseqf  34699  sseqp1  34702  fiblem  34705  fibp1  34708  cvmseu  35639  cvmliftmolem1  35644  cvmliftmolem2  35645  cvmliftlem15  35661  cvmlift2lem10  35675  cvmlift3lem8  35689  elmthm  35939  mthmblem  35943  mclsppslem  35946  mclspps  35947  cnambfre  38179  dvtan  38181  ftc1anclem3  38206  ftc1anclem5  38208  areacirc  38224  sstotbnd2  38285  keridl  38543  ellkr  39725  pw2f1ocnv  43626  binomcxplemdvbinom  44927  binomcxplemcvg  44928  binomcxplemnotnn0  44930  permaxpow  45583  rfcnpre1  45597  rfcnpre2  45609  rfcnpre3  45611  rfcnpre4  45612  limsupresxr  46338  liminfresxr  46339  icccncfext  46459  sge0fodjrnlem  46988  smfsuplem1  47383