![]() |
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 2611 | . 2 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V) | |
3 | 1, 2 | ax-mp 7 | 1 ⊢ 𝐴 ∈ V |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 1434 Vcvv 2602 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1377 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-4 1441 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-ext 2064 |
This theorem depends on definitions: df-bi 115 df-sb 1687 df-clab 2069 df-cleq 2075 df-clel 2078 df-v 2604 |
This theorem is referenced by: onunisuci 4189 ordsoexmid 4307 fnoei 6090 oeiexg 6091 1domsn 6353 endisj 6358 unfiexmid 6428 pm54.43 6508 indpi 6583 prarloclemarch2 6660 prarloclemlt 6734 opelreal 7047 elreal 7048 elreal2 7050 eqresr 7055 c0ex 7164 1ex 7165 pnfex 7223 2ex 8167 3ex 8171 elxr 8917 |
Copyright terms: Public domain | W3C validator |