Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > elmapd | Structured version Visualization version GIF version |
Description: Deduction form of elmapg 8408. (Contributed by BJ, 11-Apr-2020.) |
Ref | Expression |
---|---|
elmapd.a | ⊢ (𝜑 → 𝐴 ∈ 𝑉) |
elmapd.b | ⊢ (𝜑 → 𝐵 ∈ 𝑊) |
Ref | Expression |
---|---|
elmapd | ⊢ (𝜑 → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶:𝐵⟶𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elmapd.a | . 2 ⊢ (𝜑 → 𝐴 ∈ 𝑉) | |
2 | elmapd.b | . 2 ⊢ (𝜑 → 𝐵 ∈ 𝑊) | |
3 | elmapg 8408 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶:𝐵⟶𝐴)) | |
4 | 1, 2, 3 | syl2anc 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 |