Theorem elpreima 7083

Description: Membership in the preimage of a class under a function. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Sky Winter, 22-Oct-2026.)

Assertion

Ref	Expression
elpreima	⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) ↔ (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))

Proof of Theorem elpreima

Step	Hyp	Ref	Expression
1		cnvimass 6212	. . . . 5 ⊢ (◡𝐹 “ 𝐶) ⊆ dom 𝐹
2	1	sseli 3909	. . . 4 ⊢ (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ dom 𝐹)
3		fndm 6667	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
4	3	eleq2d 2850	. . . 4 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴))
5	2, 4	imbitrid 247	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ 𝐴))
6	5	pm4.71rd 572	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) ↔ (𝐵 ∈ 𝐴 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶))))
7		fvimacnv 7078	. . . 4 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
8	7	funfni 6670	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶)))
9	8	pm5.32da 590	. 2 ⊢ (𝐹 Fn 𝐴 → ((𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶) ↔ (𝐵 ∈ 𝐴 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶))))
10	6, 9	bitr4d 285	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) ↔ (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2147  ^◡ccnv 5655  dom cdm 5656   “ cima 5659   Fn wfn 6556  ‘cfv 6561

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-nul 5264  ax-pr 5396

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5172  df-id 5551  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-iota 6515  df-fun 6563  df-fn 6564  df-fv 6569

This theorem is used by:  elpreimad  7085  fniniseg  7086  fncnvima2  7087  unpreima  7089  respreima  7092  fnse  8180  brwitnlem  8546  unxpwdom2  9612  smobeth  10701  fpwwe2lem5  10750  hashkf  14506  isercolllem2  15865  isercolllem3  15866  isercoll  15867  fsumss  15923  fprodss  16147  tanval  16328  1arith  17137  0ram  17230  ghmpreima  19484  ghmnsgpreima  19487  kerf1ghm  19493  torsubg  20101  lmhmpreima  21356  rhmpreimaidl  21604  rhmpreimaprmidl  21668  znunithash  21903  mpfind  22457  cncnpi  23629  cncnp  23631  cnpdis  23644  cnt0  23697  cnhaus  23705  2ndcomap  23810  1stccnp  23814  ptpjpre1  23923  tx1cn  23961  tx2cn  23962  txcnmpt  23976  txdis1cn  23987  hauseqlcld  23998  xkoptsub  24006  xkococn  24012  kqsat  24083  kqcldsat  24085  kqreglem1  24093  kqreglem2  24094  reghmph  24145  ordthmeolem  24153  tmdcn2  24441  clssubg  24461  tgphaus  24469  qustgplem  24473  ucncn  24636  xmeterval  24784  imasf1obl  24840  blval2  24914  metuel2  24917  isnghm  25075  cnbl0  25125  cnblcld  25126  cnheiborlem  25308  nmhmcn  25474  ismbl  25880  mbfeqalem1  25995  mbfmulc2lem  26001  mbfmax  26003  mbfposr  26006  mbfimaopnlem  26009  mbfaddlem  26014  mbfsup  26018  i1f1lem  26043  i1fpos  26060  mbfi1fseqlem4  26072  itg2monolem1  26104  itg2gt0  26114  itg2cnlem1  26115  itg2cnlem2  26116  plyeq0lem  26562  dgrlem  26581  dgrub  26586  dgrlb  26588  pserulm  26782  psercnlem2  26784  psercnlem1  26785  psercn  26786  abelth  26801  eff1olem  26909  ellogrn  26920  dvloglem  27009  logf1o2  27011  efopnlem1  27017  efopnlem2  27018  logtayl  27021  cxpcn3lem  27108  cxpcn3  27109  resqrtcn  27110  asinneg  27247  areambl  27319  sqff1o  27542  ubthlem1  31505  unipreima  33312  suppiniseg  33353  1stpreima  33374  2ndpreima  33375  suppss3  33388  hashgt1  33473  pwrssmgc  33637  tocyc01  33755  cyc3evpm  33787  elrgspnsubrunlem2  33885  kerunit  33970  elrspunidl  34062  ply1degltel  34209  ply1degleel  34210  ply1degltdimlem  34337  irngnminplynz  34427  smatrcl  34511  rhmpreimacnlem  34599  cnre2csqlem  34625  elzrhunit  34692  qqhval2lem  34696  qqhf  34701  1stmbfm  34975  2ndmbfm  34976  mbfmcnt  34983  eulerpartlemsv2  35073  eulerpartlemv  35079  eulerpartlemf  35085  eulerpartlemgvv  35091  eulerpartlemgh  35093  eulerpartlemgs2  35095  sseqmw  35106  sseqf  35107  sseqp1  35110  fiblem  35113  fibp1  35116  cvmseu  36221  cvmliftmolem1  36226  cvmliftmolem2  36227  cvmliftlem15  36243  cvmlift2lem10  36257  cvmlift3lem8  36271  elmthm  36521  mthmblem  36525  mclsppslem  36528  mclspps  36529  cnambfre  38791  dvtan  38793  ftc1anclem3  38818  ftc1anclem5  38820  areacirc  38836  sstotbnd2  38911  keridl  39169  ellkr  40349  pw2f1ocnv  44248  binomcxplemdvbinom  45540  binomcxplemcvg  45541  binomcxplemnotnn0  45543  permaxpow  46205  rfcnpre1  46252  rfcnpre2  46264  rfcnpre3  46266  rfcnpre4  46267  limsupresxr  46991  liminfresxr  46992  icccncfext  47112  sge0fodjrnlem  47641  smfsuplem1  48036  tanhval  51131  tanhf  51133  tanhcl  51134