![]() |
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, then it is a set. Deduction associated with elex 3428. (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 3428 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2166 Vcvv 3413 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-12 2222 ax-ext 2802 |
This theorem depends on definitions: df-bi 199 df-an 387 df-tru 1662 df-ex 1881 df-sb 2070 df-clab 2811 df-cleq 2817 df-clel 2820 df-v 3415 |
This theorem is referenced by: reuhypd 5122 ideqg 5505 elrnmptg 5607 fvmptd3f 6541 mapsnend 8300 strfv2d 16267 estrres 17131 pospropd 17486 gsumvalx 17622 isunit 19010 israg 26008 structtocusgr 26743 1loopgrnb0 26799 iswlkg 26910 funcnvmpt 30015 sitgval 30938 breprexplema 31256 bnj1463 31668 wsuclem 32308 rfovd 39134 fsovd 39141 fsovrfovd 39142 dssmapfvd 39150 limsupvaluz 40734 limsupequzmpt2 40744 limsupvaluz2 40764 liminfequzmpt2 40817 rrxsnicc 41310 ioorrnopnlem 41314 ioorrnopnxrlem 41316 subsaliuncl 41366 sge0xaddlem1 41440 sge0xaddlem2 41441 sge0xadd 41442 sge0splitsn 41448 meaiininclem 41493 hoicvrrex 41563 ovn0lem 41572 hoidmvlelem3 41604 ovnhoilem1 41608 hoicoto2 41612 hoidifhspval3 41626 hoiqssbllem1 41629 ovolval4lem1 41656 vonvolmbl 41668 iinhoiicclem 41680 iunhoiioolem 41682 vonioolem1 41687 vonioolem2 41688 vonicclem1 41690 vonicclem2 41691 decsmf 41768 smflimlem4 41775 smfmullem4 41794 smfco 41802 smfpimcclem 41806 smflimsupmpt 41828 smfliminfmpt 41831 opabresex0d 42187 setsnidel 42234 isupwlkg 42564 |
Copyright terms: Public domain | W3C validator |