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

Theorem elmapd 7374
Description: Deduction form of elmapg 7373. (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 7373 . 2  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( C  e.  ( A  ^m  B )  <-> 
C : B --> A ) )
41, 2, 3syl2anc 659 1  |-  ( ph  ->  ( C  e.  ( A  ^m  B )  <-> 
C : B --> A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    e. wcel 1836   -->wf 5509  (class class class)co 6218    ^m cmap 7360
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2020  ax-ext 2374  ax-sep 4505  ax-nul 4513  ax-pow 4560  ax-pr 4618  ax-un 6513
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2236  df-mo 2237  df-clab 2382  df-cleq 2388  df-clel 2391  df-nfc 2546  df-ne 2593  df-ral 2751  df-rex 2752  df-rab 2755  df-v 3053  df-sbc 3270  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3729  df-if 3875  df-pw 3946  df-sn 3962  df-pr 3964  df-op 3968  df-uni 4181  df-br 4385  df-opab 4443  df-id 4726  df-xp 4936  df-rel 4937  df-cnv 4938  df-co 4939  df-dm 4940  df-rn 4941  df-iota 5477  df-fun 5515  df-fn 5516  df-f 5517  df-fv 5521  df-ov 6221  df-oprab 6222  df-mpt2 6223  df-map 7362
This theorem is referenced by:  elmapssres  7384  mapss  7402  ralxpmap  7409  mapen  7622  mapunen  7627  f1finf1o  7684  mapfienlem3  7803  mapfien  7804  cantnfs  8020  acni  8361  infmap2  8533  fin23lem32  8659  iundom2g  8850  wunf  9038  hashf1lem1  12431  hashf1lem2  12432  prdsplusg  14888  prdsmulr  14889  prdsvsca  14890  elsetchom  15500  setcco  15502  isga  16469  evls1sca  18496  mamures  19000  mat1dimmul  19086  1mavmul  19158  mdetunilem9  19230  cnpdis  19903  xkopjcn  20265  indishmph  20407  tsmsxplem2  20764  dchrfi  23670  fcobij  27732  mbfmcst  28426  1stmbfm  28427  2ndmbfm  28428  mbfmco  28431  sibfof  28505  mapco2g  30852  elmapresaun  30909  dvnprodlem1  31948  fourierdlem14  32108  fourierdlem15  32109  fourierdlem81  32175  fourierdlem92  32186  el0ldep  33306
  Copyright terms: Public domain W3C validator