![]() |
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 8213. (Contributed by BJ, 11-Apr-2020.) |
Ref | Expression |
---|---|
elmapd.a | ⊢ (𝜑 → 𝐴 ∈ 𝑉) |
elmapd.b | ⊢ (𝜑 → 𝐵 ∈ 𝑊) |
Ref | Expression |
---|---|
elmapd | ⊢ (𝜑 → (𝐶 ∈ (𝐴 ↑𝑚 𝐵) ↔ 𝐶:𝐵⟶𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elmapd.a | . 2 ⊢ (𝜑 → 𝐴 ∈ 𝑉) | |
2 | elmapd.b | . 2 ⊢ (𝜑 → 𝐵 ∈ 𝑊) | |
3 | elmapg 8213 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑𝑚 𝐵) ↔ 𝐶:𝐵⟶𝐴)) | |
4 | 1, 2, 3 | syl2anc 576 | 1 ⊢ (𝜑 → (𝐶 ∈ (𝐴 ↑𝑚 𝐵) ↔ 𝐶:𝐵⟶𝐴)) |
Colors of variables: wff setvar class |
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 |
Copyright terms: Public domain | W3C validator |