![]() |
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 2160 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | alrimiv 1803 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | elisset 2636 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | exim 1536 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 2, 3, 4 | sylc 62 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1382 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-8 1441 ax-4 1446 ax-17 1465 ax-i9 1469 ax-ial 1473 ax-ext 2071 |
This theorem depends on definitions: df-bi 116 df-sb 1694 df-clab 2076 df-cleq 2082 df-clel 2085 df-v 2624 |
This theorem is referenced by: snmg 3566 oprcl 3654 exmid01 4040 exss 4065 onintrab2im 4350 regexmidlemm 4363 acexmidlem2 5665 frecabcl 6180 ixpm 6503 enm 6592 ssfilem 6647 fin0 6657 fin0or 6658 diffitest 6659 diffisn 6665 infm 6676 inffiexmid 6678 exmidfodomrlemr 6891 exmidfodomrlemrALT 6892 caucvgsrlemasr 7398 gtso 7627 indstr 9144 negm 9163 fzm 9515 fzom 9638 rexfiuz 10485 r19.2uz 10489 resqrexlemgt0 10516 climuni 10744 bezoutlembi 11335 lcmgcdlem 11400 nninfall 12203 |
Copyright terms: Public domain | W3C validator |