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

Theorem elmapd 7491
Description: Deduction form of elmapg 7490. (Contributed by BJ, 11-Apr-2020.)
Hypotheses
Ref Expression
elmapd.a  |-  ( ph  ->  A  e.  V )
elmapd.b  |-  ( ph  ->  B  e.  W )
Assertion
Ref Expression
elmapd  |-  ( ph  ->  ( C  e.  ( A  ^m  B )  <-> 
C : B --> A ) )

Proof of Theorem elmapd
StepHypRef Expression
1 elmapd.a . 2  |-  ( ph  ->  A  e.  V )
2 elmapd.b . 2  |-  ( ph  ->  B  e.  W )
3 elmapg 7490 . 2  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( C  e.  ( A  ^m  B )  <-> 
C : B --> A ) )
41, 2, 3syl2anc 667 1  |-  ( ph  ->  ( C  e.  ( A  ^m  B )  <-> 
C : B --> A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    e. wcel 1889   -->wf 5581  (class class class)co 6295    ^m cmap 7477
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528  ax-nul 4537  ax-pow 4584  ax-pr 4642  ax-un 6588
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-ral 2744  df-rex 2745  df-rab 2748  df-v 3049  df-sbc 3270  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3734  df-if 3884  df-pw 3955  df-sn 3971  df-pr 3973  df-op 3977  df-uni 4202  df-br 4406  df-opab 4465  df-id 4752  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-iota 5549  df-fun 5587  df-fn 5588  df-f 5589  df-fv 5593  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-map 7479
This theorem is referenced by:  elmapssres  7501  mapss  7519  ralxpmap  7526  mapen  7741  mapunen  7746  f1finf1o  7803  mapfienlem3  7925  mapfien  7926  cantnfs  8176  acni  8481  infmap2  8653  fin23lem32  8779  iundom2g  8970  wunf  9157  hashf1lem1  12625  hashf1lem2  12626  prdsplusg  15368  prdsmulr  15369  prdsvsca  15370  elsetchom  15988  setcco  15990  isga  16957  evls1sca  18924  mamures  19427  mat1dimmul  19513  1mavmul  19585  mdetunilem9  19657  cnpdis  20321  xkopjcn  20683  indishmph  20825  tsmsxplem2  21180  dchrfi  24195  fcobij  28322  mbfmcst  29093  1stmbfm  29094  2ndmbfm  29095  mbfmco  29098  sibfof  29185  mapco2g  35568  elmapresaun  35625  dvnprodlem1  37831  fourierdlem14  37993  fourierdlem15  37994  fourierdlem81  38061  fourierdlem92  38072  hoidmvlelem3  38429  el0ldep  40363
  Copyright terms: Public domain W3C validator