Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > elrabi | Unicode version |
Description: Implication for the membership in a restricted class abstraction. (Contributed by Alexander van der Vekens, 31-Dec-2017.) |
Ref | Expression |
---|---|
elrabi |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | clelab 2265 | . . 3 | |
2 | eleq1 2202 | . . . . . 6 | |
3 | 2 | anbi1d 460 | . . . . 5 |
4 | 3 | simprbda 380 | . . . 4 |
5 | 4 | exlimiv 1577 | . . 3 |
6 | 1, 5 | sylbi 120 | . 2 |
7 | df-rab 2425 | . 2 | |
8 | 6, 7 | eleq2s 2234 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wceq 1331 wex 1468 wcel 1480 cab 2125 crab 2420 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-11 1484 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-ext 2121 |
This theorem depends on definitions: df-bi 116 df-nf 1437 df-sb 1736 df-clab 2126 df-cleq 2132 df-clel 2135 df-rab 2425 |
This theorem is referenced by: ordtriexmidlem 4435 ordtri2or2exmidlem 4441 onsucelsucexmidlem 4444 ordsoexmid 4477 reg3exmidlemwe 4493 elfvmptrab1 5515 acexmidlemcase 5769 ssfirab 6822 exmidonfinlem 7049 genpelvl 7320 genpelvu 7321 suplocsrlempr 7615 nnindnn 7701 sup3exmid 8715 nnind 8736 supinfneg 9390 infsupneg 9391 supminfex 9392 ublbneg 9405 hashinfuni 10523 zsupcllemstep 11638 infssuzex 11642 infssuzledc 11643 bezoutlemsup 11697 lcmgcdlem 11758 oddennn 11905 evenennn 11906 znnen 11911 ennnfonelemg 11916 txdis1cn 12447 reopnap 12707 divcnap 12724 limccl 12797 dvlemap 12818 dvaddxxbr 12834 dvmulxxbr 12835 dvcoapbr 12840 dvcjbr 12841 dvrecap 12846 dveflem 12855 |
Copyright terms: Public domain | W3C validator |