![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ovexi | Structured version Visualization version GIF version |
Description: The result of an operation is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
Ref | Expression |
---|---|
ovexi.1 | ⊢ 𝐴 = (𝐵𝐹𝐶) |
Ref | Expression |
---|---|
ovexi | ⊢ 𝐴 ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ovexi.1 | . 2 ⊢ 𝐴 = (𝐵𝐹𝐶) | |
2 | ovex 7448 | . 2 ⊢ (𝐵𝐹𝐶) ∈ V | |
3 | 1, 2 | eqeltri 2825 | 1 ⊢ 𝐴 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1534 ∈ wcel 2099 Vcvv 3470 (class class class)co 7415 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699 ax-nul 5301 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-ne 2937 df-v 3472 df-dif 3948 df-un 3950 df-in 3952 df-ss 3962 df-nul 4320 df-sn 4626 df-pr 4628 df-uni 4905 df-iota 6495 df-fv 6551 df-ov 7418 |
This theorem is referenced by: negex 11483 decex 12706 cshwsexaOLD 14802 eulerthlem2 16745 subccatid 17826 funcres2c 17884 ressffth 17921 fuccofval 17944 fuchom 17946 fuchomOLD 17947 fuccatid 17955 xpccatid 18173 gsumress 18636 prdssgrpd 18687 smndex1mgm 18853 eqgen 19130 quselbas 19133 quseccl0 19134 qus0subgbas 19147 orbsta 19258 sylow2blem1 19569 sylow2blem2 19570 frgpnabllem1 19822 rngqipbas 21179 rngqiprngimf 21181 rngqiprngghm 21183 rngqiprngimf1 21184 rngqiprnglin 21186 rngqiprngim 21188 rngqiprngfulem1 21195 znle 21460 znbas 21471 znzrhval 21474 relt 21541 retos 21544 frlmlbs 21725 lsslindf 21758 lsslinds 21759 uvcendim 21775 subrgmvr 21965 opsrle 21979 subrgascl 22004 evl1fval 22241 matgsum 22333 matmulr 22334 scmatghm 22429 marepvfval 22461 m2cpmmhm 22641 cpm2mfval 22645 cpmadumatpolylem2 22778 cldsubg 24009 nghmfval 24633 pi1bas 24959 dv11cn 25928 quotval 26221 pserdvlem2 26359 ang180lem3 26737 dchrptlem2 27192 usgrexmpllem 29067 nbusgrf1o1 29177 crctcshlem3 29624 2pthon3v 29748 konigsberglem5 30060 konigsberg 30061 bloval 30585 dpval 32608 rlocbas 32976 rloccring 32979 rloc0g 32980 rloc1r 32981 rlocf1 32982 zringfrac 32991 evls1vsca 33246 asclply1subcl 33252 resssra 33278 qusdimsum 33317 satfv1fvfmla1 35028 2goelgoanfmla1 35029 satefvfmla1 35030 cdleme31snd 39854 evlsvvvallem2 41786 evlsvvval 41787 evlsmhpvvval 41819 mhphf 41821 c0exALT 41825 prjcrvfval 42046 prjcrvval 42047 mnringmulrd 43649 subsalsal 45738 naryfvalixp 47693 naryfvalelfv 47696 rrxline 47798 inlinecirc02p 47851 inlinecirc02preu 47852 |
Copyright terms: Public domain | W3C validator |