Theorem elmapd 8214

Description: Deduction form of elmapg 8213. (Contributed by BJ, 11-Apr-2020.)

Hypotheses

Ref	Expression
elmapd.a	⊢ (𝜑 → 𝐴 ∈ 𝑉)
elmapd.b	⊢ (𝜑 → 𝐵 ∈ 𝑊)

Assertion

Ref	Expression
elmapd	⊢ (𝜑 → (𝐶 ∈ (𝐴 ↑𝑚 𝐵) ↔ 𝐶:𝐵⟶𝐴))

Proof of Theorem elmapd

Step	Hyp	Ref	Expression
1		elmapd.a	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
2		elmapd.b	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝑊)
3		elmapg 8213	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑𝑚 𝐵) ↔ 𝐶:𝐵⟶𝐴))
4	1, 2, 3	syl2anc 576	1 ⊢ (𝜑 → (𝐶 ∈ (𝐴 ↑𝑚 𝐵) ↔ 𝐶:𝐵⟶𝐴))

Syntax hints:   → wi 4   ↔ wb 198   ∈ wcel 2050  ⟶wf 6178  (class class class)co 6970   ↑_𝑚 cmap 8200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2744  ax-sep 5054  ax-nul 5061  ax-pow 5113  ax-pr 5180  ax-un 7273

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ral 3087  df-rex 3088  df-rab 3091  df-v 3411  df-sbc 3676  df-dif 3826  df-un 3828  df-in 3830  df-ss 3837  df-nul 4173  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-op 4442  df-uni 4707  df-br 4924  df-opab 4986  df-id 5306  df-xp 5407  df-rel 5408  df-cnv 5409  df-co 5410  df-dm 5411  df-rn 5412  df-iota 6146  df-fun 6184  df-fn 6185  df-f 6186  df-fv 6190  df-ov 6973  df-oprab 6974  df-mpo 6975  df-map 8202

This theorem is referenced by:  elmapssres  8225  mapsnd  8242  mapss  8245  ralxpmap  8252  mapen  8471  mapunen  8476  f1finf1o  8534  mapfienlem3  8659  mapfien  8660  cantnfs  8917  acni  9259  infmap2  9432  fin23lem32  9558  iundom2g  9754  wunf  9941  hashf1lem1  13620  hashf1lem2  13621  prdsplusg  16581  prdsmulr  16582  prdsvsca  16583  elsetchom  17193  setcco  17195  elestrchom  17230  estrcco  17232  funcsetcestrclem7  17263  isga  18186  evls1sca  20183  frlmvplusgvalc  20607  frlmplusgvalb  20609  frlmvscavalb  20610  mamures  20697  mat1dimmul  20783  1mavmul  20855  mdetunilem9  20927  cnpdis  21599  xkopjcn  21962  indishmph  22104  tsmsxplem2  22459  rrx0el  23698  dchrfi  25527  fcobij  30211  rmfsupp2  30545  linds2eq  30612  lbsdiflsp0  30651  fedgmullem1  30654  fedgmullem2  30655  fedgmul  30656  mbfmcst  31162  1stmbfm  31163  2ndmbfm  31164  mbfmco  31167  sibfof  31243  frlmfielbas  38576  mapco2g  38706  elmapresaun  38763  rfovcnvf1od  39713  fsovfd  39721  fsovcnvlem  39722  dssmapnvod  39729  clsk3nimkb  39753  ntrelmap  39838  clselmap  39840  k0004lem2  39861  elmapsnd  40892  mapss2  40893  unirnmap  40896  inmap  40897  difmapsn  40900  unirnmapsn  40902  dvnprodlem1  41661  fourierdlem14  41837  fourierdlem15  41838  fourierdlem81  41903  fourierdlem92  41914  rrnprjdstle  42017  subsaliuncllem  42071  hoidmvlelem3  42310  ovolval2lem  42356  ovolval4lem2  42363  ovolval5lem2  42366  ovnovollem1  42369  smfmullem4  42500  el0ldep  43888