| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > elex2 | Unicode version | ||
| Description: If a class contains another class, then it contains some set. (Contributed by Alan Sare, 25-Sep-2011.) |
| Ref | Expression |
|---|---|
| elex2 |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eleq1a 2303 |
. . 3
| |
| 2 | 1 | alrimiv 1922 |
. 2
|
| 3 | elisset 2817 |
. 2
| |
| 4 | exim 1647 |
. 2
| |
| 5 | 2, 3, 4 | sylc 62 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| 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 1495 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-ext 2213 |
| This theorem depends on definitions: df-bi 117 df-sb 1811 df-clab 2218 df-cleq 2224 df-clel 2227 df-v 2804 |
| This theorem is referenced by: snmg 3790 oprcl 3886 brm 4139 ss1o0el1 4287 exss 4319 onintrab2im 4616 regexmidlemm 4630 reldmm 4950 dmxpid 4953 acexmidlem2 6015 elmpom 6403 frecabcl 6565 ixpm 6899 en1m 6979 dom1o 7002 dom1oi 7003 enm 7004 ssfilem 7062 ssfilemd 7064 fin0 7074 fin0or 7075 diffitest 7076 diffisn 7082 infm 7096 inffiexmid 7098 ctssdc 7312 omct 7316 ctssexmid 7349 exmidfodomrlemr 7413 exmidfodomrlemrALT 7414 acnrcl 7416 exmidaclem 7423 iftrueb01 7441 pw1if 7443 caucvgsrlemasr 8010 suplocsrlempr 8027 gtso 8258 sup3exmid 9137 indstr 9827 negm 9849 fzm 10273 fzom 10400 rexfiuz 11567 r19.2uz 11571 resqrexlemgt0 11598 climuni 11871 bezoutlembi 12594 nninfct 12630 lcmgcdlem 12667 pcprecl 12880 pc2dvds 12921 4sqlem13m 12994 nninfdclemcl 13087 dfgrp3m 13700 issubg2m 13794 issubgrpd2 13795 issubg3 13797 issubg4m 13798 grpissubg 13799 subgintm 13803 nmzsubg 13815 ghmrn 13862 ghmpreima 13871 dvdsr02 14138 01eq0ring 14222 subrgugrp 14273 lmodfopnelem1 14357 rmodislmodlem 14383 rmodislmod 14384 lss1 14395 lsssubg 14410 islss3 14412 islss4 14415 lss1d 14416 lssintclm 14417 dflidl2rng 14514 lidlsubg 14519 cnsubglem 14612 tgioo 15297 elply2 15478 edgval 15930 wlkvtxm 16210 pw1nct 16655 nninfall 16662 nnnninfen 16674 |
| Copyright terms: Public domain | W3C validator |