![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > elexi | GIF version |
Description: If a class is a member of another class, it is a set. (Contributed by NM, 11-Jun-1994.) |
Ref | Expression |
---|---|
elisseti.1 | ⊢ 𝐴 ∈ 𝐵 |
Ref | Expression |
---|---|
elexi | ⊢ 𝐴 ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elisseti.1 | . 2 ⊢ 𝐴 ∈ 𝐵 | |
2 | elex 2763 | . 2 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝐴 ∈ V |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 2160 Vcvv 2752 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1458 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-v 2754 |
This theorem is referenced by: elpwi2 4176 onunisuci 4450 ordsoexmid 4579 1oex 6450 fnoei 6478 oeiexg 6479 endisj 6851 unfiexmid 6947 snexxph 6980 djuex 7073 0ct 7137 nninfex 7151 infnninfOLD 7154 nnnninf 7155 ctssexmid 7179 nninfdcinf 7200 nninfwlporlem 7202 nninfwlpoimlemg 7204 pm54.43 7220 pw1ne3 7260 3nsssucpw1 7266 2omotaplemst 7288 prarloclemarch2 7449 opelreal 7857 elreal 7858 elreal2 7860 eqresr 7866 c0ex 7982 1ex 7983 pnfex 8042 sup3exmid 8945 2ex 9022 3ex 9026 elxr 9808 setsslid 12566 setsslnid 12567 prdsex 12777 rmodislmod 13684 fnpsr 13962 lgsdir2lem3 14909 subctctexmid 15229 0nninf 15232 nninffeq 15248 |
Copyright terms: Public domain | W3C validator |