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

Theorem elmapd 8409
Description: Deduction form of elmapg 8408. (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 8408 . 2 ((𝐴𝑉𝐵𝑊) → (𝐶 ∈ (𝐴m 𝐵) ↔ 𝐶:𝐵𝐴))
41, 2, 3syl2anc 584 1 (𝜑 → (𝐶 ∈ (𝐴m 𝐵) ↔ 𝐶:𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wcel 2105  wf 6344  (class class class)co 7145  m cmap 8395
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-fv 6356  df-ov 7148  df-oprab 7149  df-mpo 7150  df-map 8397
This theorem is referenced by:  elmapssres  8420  elmapresaun  8433  mapsnd  8438  mapss  8441  ralxpmap  8448  mapen  8669  mapunen  8674  f1finf1o  8733  mapfienlem3  8858  mapfien  8859  cantnfs  9117  acni  9459  infmap2  9628  fin23lem32  9754  iundom2g  9950  wunf  10137  hashf1lem1  13801  hashf1lem2  13802  prdsplusg  16719  prdsmulr  16720  prdsvsca  16721  elsetchom  17329  setcco  17331  elestrchom  17366  estrcco  17368  funcsetcestrclem7  17399  isga  18359  evls1sca  20414  frlmvplusgvalc  20839  frlmplusgvalb  20841  frlmvscavalb  20842  mamures  20929  mat1dimmul  21013  1mavmul  21085  mdetunilem9  21157  cnpdis  21829  xkopjcn  22192  indishmph  22334  tsmsxplem2  22689  rrx0el  23928  dchrfi  25758  fcobij  30384  rmfsupp2  30793  linds2eq  30868  lbsdiflsp0  30921  fedgmullem1  30924  fedgmullem2  30925  fedgmul  30926  mbfmcst  31416  1stmbfm  31417  2ndmbfm  31418  mbfmco  31421  sibfof  31497  satfv1lem  32506  ex-sategoelel  32565  ex-sategoelelomsuc  32570  selvval2lem4  39014  selvval2lem5  39015  frlmfielbas  39017  mapco2g  39189  rfovcnvf1od  40228  fsovfd  40236  fsovcnvlem  40237  dssmapnvod  40244  clsk3nimkb  40268  ntrelmap  40353  clselmap  40355  k0004lem2  40376  elmapsnd  41343  mapss2  41344  unirnmap  41347  inmap  41348  difmapsn  41351  unirnmapsn  41353  dvnprodlem1  42107  fourierdlem14  42283  fourierdlem15  42284  fourierdlem81  42349  fourierdlem92  42360  rrnprjdstle  42463  subsaliuncllem  42517  hoidmvlelem3  42756  ovolval2lem  42802  ovolval4lem2  42809  ovolval5lem2  42812  ovnovollem1  42815  smfmullem4  42946  elefmndbas  43971  elefmndbas2  43972  symgsubmefmndALT  43996  el0ldep  44449
  Copyright terms: Public domain W3C validator