![]() |
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 2748 | . 2 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝐴 ∈ V |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 2148 Vcvv 2737 |
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 1447 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-v 2739 |
This theorem is referenced by: elpwi2 4155 onunisuci 4429 ordsoexmid 4558 1oex 6419 fnoei 6447 oeiexg 6448 endisj 6818 unfiexmid 6911 snexxph 6943 djuex 7036 0ct 7100 nninfex 7114 infnninfOLD 7117 nnnninf 7118 ctssexmid 7142 nninfdcinf 7163 nninfwlporlem 7165 nninfwlpoimlemg 7167 pm54.43 7183 pw1ne3 7223 3nsssucpw1 7229 2omotaplemst 7248 prarloclemarch2 7409 opelreal 7817 elreal 7818 elreal2 7820 eqresr 7826 c0ex 7942 1ex 7943 pnfex 8001 sup3exmid 8903 2ex 8980 3ex 8984 elxr 9763 setsslid 12495 setsslnid 12496 lgsdir2lem3 14098 subctctexmid 14406 0nninf 14409 nninffeq 14425 |
Copyright terms: Public domain | W3C validator |