Theorem elpreima 7049

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 6076	. . . . 5 ⊢ (◡𝐹 “ 𝐶) ⊆ dom 𝐹
2	1	sseli 3927	. . . 4 ⊢ (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ dom 𝐹)
3		fndm 6634	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2847	. . . 4 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴))
5	2, 4	imbitrid 247	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ 𝐴))
6		fnfun 6631	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
7		fvimacnvi 7043	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
8	6, 7	sylan 592	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶)
9	8	ex 418	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐹‘𝐵) ∈ 𝐶))
10	5, 9	jcad 522	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))
11		fvimacnv 7044	. . . . 5 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
12	11	funfni 6637	. . . 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 5650  dom cdm 5651   “ cima 5654  Fun wfun 6525   Fn wfn 6526  ‘cfv 6531

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 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6487  df-fun 6533  df-fn 6534  df-fv 6539

This theorem is used by:  elpreimad  7050  fniniseg  7051  fncnvima2  7052  unpreima  7054  respreima  7057  fnse  8134  brwitnlem  8499  unxpwdom2  9566  smobeth  10652  fpwwe2lem5  10701  hashkf  14456  isercolllem2  15813  isercolllem3  15814  isercoll  15815  fsumss  15871  fprodss  16095  tanval  16276  1arith  17085  0ram  17178  ghmpreima  19432  ghmnsgpreima  19435  kerf1ghm  19441  torsubg  20048  lmhmpreima  21303  rhmpreimaidl  21551  rhmpreimaprmidl  21615  znunithash  21850  mpfind  22404  cncnpi  23576  cncnp  23578  cnpdis  23591  cnt0  23644  cnhaus  23652  2ndcomap  23757  1stccnp  23761  ptpjpre1  23870  tx1cn  23908  tx2cn  23909  txcnmpt  23923  txdis1cn  23934  hauseqlcld  23945  xkoptsub  23953  xkococn  23959  kqsat  24030  kqcldsat  24032  kqreglem1  24040  kqreglem2  24041  reghmph  24092  ordthmeolem  24100  tmdcn2  24388  clssubg  24408  tgphaus  24416  qustgplem  24420  ucncn  24583  xmeterval  24731  imasf1obl  24787  blval2  24861  metuel2  24864  isnghm  25022  cnbl0  25072  cnblcld  25073  cnheiborlem  25255  nmhmcn  25421  ismbl  25827  mbfeqalem1  25942  mbfmulc2lem  25948  mbfmax  25950  mbfposr  25953  mbfimaopnlem  25956  mbfaddlem  25961  mbfsup  25965  i1f1lem  25990  i1fpos  26007  mbfi1fseqlem4  26019  itg2monolem1  26051  itg2gt0  26061  itg2cnlem1  26062  itg2cnlem2  26063  plyeq0lem  26509  dgrlem  26528  dgrub  26533  dgrlb  26535  pserulm  26731  psercnlem2  26733  psercnlem1  26734  psercn  26735  abelth  26750  eff1olem  26858  ellogrn  26869  dvloglem  26958  logf1o2  26960  efopnlem1  26966  efopnlem2  26967  logtayl  26970  cxpcn3lem  27057  cxpcn3  27058  resqrtcn  27059  asinneg  27196  areambl  27268  sqff1o  27491  ubthlem1  31454  unipreima  33219  suppiniseg  33261  1stpreima  33282  2ndpreima  33283  suppss3  33297  hashgt1  33382  pwrssmgc  33543  tocyc01  33661  cyc3evpm  33693  elrgspnsubrunlem2  33791  kerunit  33868  elrspunidl  33960  ply1degltel  34108  ply1degleel  34109  ply1degltdimlem  34236  irngnminplynz  34326  smatrcl  34410  rhmpreimacnlem  34498  cnre2csqlem  34524  elzrhunit  34591  qqhval2lem  34595  qqhf  34600  1stmbfm  34875  2ndmbfm  34876  mbfmcnt  34883  eulerpartlemsv2  34973  eulerpartlemv  34979  eulerpartlemf  34985  eulerpartlemgvv  34991  eulerpartlemgh  34993  eulerpartlemgs2  34995  sseqmw  35006  sseqf  35007  sseqp1  35010  fiblem  35013  fibp1  35016  cvmseu  36010  cvmliftmolem1  36015  cvmliftmolem2  36016  cvmliftlem15  36032  cvmlift2lem10  36046  cvmlift3lem8  36060  elmthm  36310  mthmblem  36314  mclsppslem  36317  mclspps  36318  cnambfre  38554  dvtan  38556  ftc1anclem3  38581  ftc1anclem5  38583  areacirc  38599  sstotbnd2  38676  keridl  38934  ellkr  40114  pw2f1ocnv  43997  binomcxplemdvbinom  45296  binomcxplemcvg  45297  binomcxplemnotnn0  45299  permaxpow  45951  rfcnpre1  45979  rfcnpre2  45991  rfcnpre3  45993  rfcnpre4  45994  limsupresxr  46720  liminfresxr  46721  icccncfext  46841  sge0fodjrnlem  47370  smfsuplem1  47765