| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > elfvexd | Structured version Visualization version GIF version | ||
| Description: If a function value has a member, then its argument is a set. Deduction form of elfvex 6944. (An artifact of our function value definition.) (Contributed by David Moews, 1-May-2017.) |
| Ref | Expression |
|---|---|
| elfvexd.1 | ⊢ (𝜑 → 𝐴 ∈ (𝐵‘𝐶)) |
| Ref | Expression |
|---|---|
| elfvexd | ⊢ (𝜑 → 𝐶 ∈ V) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elfvexd.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ (𝐵‘𝐶)) | |
| 2 | elfvex 6944 | . 2 ⊢ (𝐴 ∈ (𝐵‘𝐶) → 𝐶 ∈ V) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 𝐶 ∈ V) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2108 Vcvv 3480 ‘cfv 6561 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-nul 5306 ax-pr 5432 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-dm 5695 df-iota 6514 df-fv 6569 |
| This theorem is referenced by: mrieqv2d 17682 mreexmrid 17686 mreexexlem3d 17689 mreexexlem4d 17690 mreexexd 17691 mreexdomd 17692 acsdomd 18602 ismgmn0 18655 ecqusaddcl 19211 telgsumfz 20008 isirred 20419 tgclb 22977 alexsublem 24052 cnextcn 24075 ustssel 24214 fmucnd 24301 trcfilu 24303 cfiluweak 24304 ucnextcn 24313 imasdsf1olem 24383 imasf1oxmet 24385 comet 24526 restmetu 24583 wlkp1lem4 29694 wlkp1lem8 29698 1wlkdlem4 30159 eupth2lem3lem1 30247 eupth2lem3lem2 30248 gsumsubg 33049 opprqusplusg 33517 opprqus0g 33518 lsssra 33639 lbsdiflsp0 33677 fedgmullem1 33680 mzpcl34 42742 xlimbr 45842 xlimmnfvlem2 45848 xlimpnfvlem2 45852 elxpcbasex1ALT 48955 elxpcbasex2ALT 48957 swapf1 48978 |
| Copyright terms: Public domain | W3C validator |