![]() |
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 8036. (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 8036 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑𝑚 𝐵) ↔ 𝐶:𝐵⟶𝐴)) | |
4 | 1, 2, 3 | syl2anc 696 | 1 ⊢ (𝜑 → (𝐶 ∈ (𝐴 ↑𝑚 𝐵) ↔ 𝐶:𝐵⟶𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∈ wcel 2139 ⟶wf 6045 (class class class)co 6813 ↑𝑚 cmap 8023 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-8 2141 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 ax-sep 4933 ax-nul 4941 ax-pow 4992 ax-pr 5055 ax-un 7114 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-eu 2611 df-mo 2612 df-clab 2747 df-cleq 2753 df-clel 2756 df-nfc 2891 df-ral 3055 df-rex 3056 df-rab 3059 df-v 3342 df-sbc 3577 df-dif 3718 df-un 3720 df-in 3722 df-ss 3729 df-nul 4059 df-if 4231 df-pw 4304 df-sn 4322 df-pr 4324 df-op 4328 df-uni 4589 df-br 4805 df-opab 4865 df-id 5174 df-xp 5272 df-rel 5273 df-cnv 5274 df-co 5275 df-dm 5276 df-rn 5277 df-iota 6012 df-fun 6051 df-fn 6052 df-f 6053 df-fv 6057 df-ov 6816 df-oprab 6817 df-mpt2 6818 df-map 8025 |
This theorem is referenced by: elmapssres 8048 mapss 8066 ralxpmap 8073 mapen 8289 mapunen 8294 f1finf1o 8352 mapfienlem3 8477 mapfien 8478 cantnfs 8736 acni 9058 infmap2 9232 fin23lem32 9358 iundom2g 9554 wunf 9741 hashf1lem1 13431 hashf1lem2 13432 prdsplusg 16320 prdsmulr 16321 prdsvsca 16322 elsetchom 16932 setcco 16934 isga 17924 evls1sca 19890 mamures 20398 mat1dimmul 20484 1mavmul 20556 mdetunilem9 20628 cnpdis 21299 xkopjcn 21661 indishmph 21803 tsmsxplem2 22158 dchrfi 25179 fcobij 29809 mbfmcst 30630 1stmbfm 30631 2ndmbfm 30632 mbfmco 30635 sibfof 30711 mapco2g 37779 elmapresaun 37836 rfovcnvf1od 38800 fsovfd 38808 fsovcnvlem 38809 dssmapnvod 38816 clsk3nimkb 38840 ntrelmap 38925 clselmap 38927 k0004lem2 38948 elmapsnd 39895 mapss2 39896 unirnmap 39899 inmap 39900 difmapsn 39903 unirnmapsn 39905 dvnprodlem1 40664 fourierdlem14 40841 fourierdlem15 40842 fourierdlem81 40907 fourierdlem92 40918 rrnprjdstle 41024 subsaliuncllem 41078 hoidmvlelem3 41317 ovolval2lem 41363 ovolval4lem2 41370 ovolval5lem2 41373 ovnovollem1 41376 smfmullem4 41507 el0ldep 42765 |
Copyright terms: Public domain | W3C validator |