Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > elexd | Structured version Visualization version GIF version |
Description: If a class is a member of another class, it is a set. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
Ref | Expression |
---|---|
elexd.1 | ⊢ (𝜑 → 𝐴 ∈ 𝑉) |
Ref | Expression |
---|---|
elexd | ⊢ (𝜑 → 𝐴 ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elexd.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ 𝑉) | |
2 | elex 3212 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 1990 Vcvv 3200 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-12 2047 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-an 386 df-tru 1486 df-ex 1705 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-v 3202 |
This theorem is referenced by: reuhypd 4895 ideqg 5273 elrnmptg 5375 fvmptd3f 6295 pospropd 17134 gsumvalx 17270 isunit 18657 israg 25592 structtocusgr 26342 1loopgrnb0 26398 iswlkg 26509 sitgval 30394 breprexplema 30708 bnj1463 31123 wsuclem 31773 rfovd 38295 fsovd 38302 fsovrfovd 38303 dssmapfvd 38311 projf1o 39386 mapsnend 39391 limsupvaluz 39940 limsupequzmpt2 39950 limsupvaluz2 39970 liminfequzmpt2 40023 rrxsnicc 40520 ioorrnopnlem 40524 ioorrnopnxrlem 40526 subsaliuncl 40576 sge0xaddlem1 40650 sge0xaddlem2 40651 sge0xadd 40652 sge0splitsn 40658 meaiininclem 40700 hoiprodcl2 40769 hoicvrrex 40770 ovn0lem 40779 hoidmvlelem3 40811 ovnhoilem1 40815 hoicoto2 40819 hoidifhspval3 40833 hoiqssbllem1 40836 ovolval4lem1 40863 vonvolmbl 40875 iinhoiicclem 40887 iunhoiioolem 40889 vonioolem1 40894 vonioolem2 40895 vonicclem1 40897 vonicclem2 40898 decsmf 40975 smflimlem4 40982 smfmullem4 41001 smfco 41009 smfpimcclem 41013 smflimsuplem5 41030 smflimsupmpt 41035 smfliminfmpt 41038 opabresex0d 41304 setsnidel 41347 isupwlkg 41718 |
Copyright terms: Public domain | W3C validator |