MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elmapd Structured version   Visualization version   GIF version

Theorem elmapd 8039
Description: Deduction form of elmapg 8038. (Contributed by BJ, 11-Apr-2020.)
Hypotheses
Ref Expression
elmapd.a (𝜑𝐴𝑉)
elmapd.b (𝜑𝐵𝑊)
Assertion
Ref Expression
elmapd (𝜑 → (𝐶 ∈ (𝐴𝑚 𝐵) ↔ 𝐶:𝐵𝐴))

Proof of Theorem elmapd
StepHypRef Expression
1 elmapd.a . 2 (𝜑𝐴𝑉)
2 elmapd.b . 2 (𝜑𝐵𝑊)
3 elmapg 8038 . 2 ((𝐴𝑉𝐵𝑊) → (𝐶 ∈ (𝐴𝑚 𝐵) ↔ 𝐶:𝐵𝐴))
41, 2, 3syl2anc 696 1 (𝜑 → (𝐶 ∈ (𝐴𝑚 𝐵) ↔ 𝐶:𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wcel 2139  wf 6045  (class class class)co 6814  𝑚 cmap 8025
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-fv 6057  df-ov 6817  df-oprab 6818  df-mpt2 6819  df-map 8027
This theorem is referenced by:  elmapssres  8050  mapss  8068  ralxpmap  8075  mapen  8291  mapunen  8296  f1finf1o  8354  mapfienlem3  8479  mapfien  8480  cantnfs  8738  acni  9078  infmap2  9252  fin23lem32  9378  iundom2g  9574  wunf  9761  hashf1lem1  13451  hashf1lem2  13452  prdsplusg  16340  prdsmulr  16341  prdsvsca  16342  elsetchom  16952  setcco  16954  isga  17944  evls1sca  19910  mamures  20418  mat1dimmul  20504  1mavmul  20576  mdetunilem9  20648  cnpdis  21319  xkopjcn  21681  indishmph  21823  tsmsxplem2  22178  dchrfi  25200  fcobij  29830  mbfmcst  30651  1stmbfm  30652  2ndmbfm  30653  mbfmco  30656  sibfof  30732  mapco2g  37797  elmapresaun  37854  rfovcnvf1od  38818  fsovfd  38826  fsovcnvlem  38827  dssmapnvod  38834  clsk3nimkb  38858  ntrelmap  38943  clselmap  38945  k0004lem2  38966  elmapsnd  39913  mapss2  39914  unirnmap  39917  inmap  39918  difmapsn  39921  unirnmapsn  39923  dvnprodlem1  40682  fourierdlem14  40859  fourierdlem15  40860  fourierdlem81  40925  fourierdlem92  40936  rrnprjdstle  41042  subsaliuncllem  41096  hoidmvlelem3  41335  ovolval2lem  41381  ovolval4lem2  41388  ovolval5lem2  41391  ovnovollem1  41394  smfmullem4  41525  el0ldep  42783
  Copyright terms: Public domain W3C validator