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

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

Proof of Theorem elmapd
StepHypRef Expression
1 elmapd.a . 2 (𝜑𝐴𝑉)
2 elmapd.b . 2 (𝜑𝐵𝑊)
3 elmapg 8406 . 2 ((𝐴𝑉𝐵𝑊) → (𝐶 ∈ (𝐴m 𝐵) ↔ 𝐶:𝐵𝐴))
41, 2, 3syl2anc 587 1 (𝜑 → (𝐶 ∈ (𝐴m 𝐵) ↔ 𝐶:𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wcel 2112  wf 6324  (class class class)co 7139  m cmap 8393
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rex 3115  df-rab 3118  df-v 3446  df-sbc 3724  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-opab 5096  df-id 5428  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-fv 6336  df-ov 7142  df-oprab 7143  df-mpo 7144  df-map 8395
This theorem is referenced by:  elmapssres  8418  elmapresaun  8431  mapsnd  8437  mapss  8440  ralxpmap  8447  mapen  8669  mapunen  8674  f1finf1o  8733  mapfienlem3  8858  mapfien  8859  cantnfs  9117  acni  9460  infmap2  9633  fin23lem32  9759  iundom2g  9955  wunf  10142  hashf1lem1  13813  hashf1lem2  13814  prdsplusg  16727  prdsmulr  16728  prdsvsca  16729  elsetchom  17337  setcco  17339  elestrchom  17374  estrcco  17376  funcsetcestrclem7  17407  elefmndbas  18034  isga  18417  symgbasmap  18501  frlmvplusgvalc  20460  frlmplusgvalb  20462  frlmvscavalb  20463  evls1sca  20951  mamures  21001  mat1dimmul  21085  1mavmul  21157  mdetunilem9  21229  cnpdis  21902  xkopjcn  22265  indishmph  22407  tsmsxplem2  22763  rrx0el  24006  dchrfi  25843  fcobij  30488  rmfsupp2  30921  linds2eq  30999  elrspunidl  31018  lbsdiflsp0  31114  fedgmullem1  31117  fedgmullem2  31118  fedgmul  31119  zarcmplem  31238  mbfmcst  31631  1stmbfm  31632  2ndmbfm  31633  mbfmco  31636  sibfof  31712  satfv1lem  32723  ex-sategoelel  32782  ex-sategoelelomsuc  32787  selvval2lem4  39428  selvval2lem5  39429  frlmfielbas  39431  fsuppind  39453  fsuppssindlem2  39455  fsuppssind  39456  mapco2g  39652  rfovcnvf1od  40702  fsovfd  40710  fsovcnvlem  40711  dssmapnvod  40718  clsk3nimkb  40740  ntrelmap  40825  clselmap  40827  k0004lem2  40848  elmapsnd  41830  mapss2  41831  unirnmap  41834  inmap  41835  difmapsn  41838  unirnmapsn  41840  dvnprodlem1  42585  fourierdlem14  42760  fourierdlem15  42761  fourierdlem81  42826  fourierdlem92  42837  rrnprjdstle  42940  subsaliuncllem  42994  hoidmvlelem3  43233  ovolval2lem  43279  ovolval4lem2  43286  ovolval5lem2  43289  ovnovollem1  43292  smfmullem4  43423  fprmappr  44744  el0ldep  44872  naryfvalelfv  45043  fv1arycl  45048  1arymaptf  45052  2arymaptfo  45065
  Copyright terms: Public domain W3C validator