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 2242 | . . 3 | |
2 | eleq1 2180 | . . . . . 6 | |
3 | 2 | anbi1d 460 | . . . . 5 |
4 | 3 | simprbda 380 | . . . 4 |
5 | 4 | exlimiv 1562 | . . 3 |
6 | 1, 5 | sylbi 120 | . 2 |
7 | df-rab 2402 | . 2 | |
8 | 6, 7 | eleq2s 2212 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wceq 1316 wex 1453 wcel 1465 cab 2103 crab 2397 |
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 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-11 1469 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-nf 1422 df-sb 1721 df-clab 2104 df-cleq 2110 df-clel 2113 df-rab 2402 |
This theorem is referenced by: ordtriexmidlem 4405 ordtri2or2exmidlem 4411 onsucelsucexmidlem 4414 ordsoexmid 4447 reg3exmidlemwe 4463 elfvmptrab1 5483 acexmidlemcase 5737 ssfirab 6790 exmidonfinlem 7017 genpelvl 7288 genpelvu 7289 suplocsrlempr 7583 nnindnn 7669 sup3exmid 8683 nnind 8704 supinfneg 9358 infsupneg 9359 supminfex 9360 ublbneg 9373 hashinfuni 10491 zsupcllemstep 11565 infssuzex 11569 infssuzledc 11570 bezoutlemsup 11624 lcmgcdlem 11685 oddennn 11832 evenennn 11833 znnen 11838 ennnfonelemg 11843 txdis1cn 12374 reopnap 12634 divcnap 12651 limccl 12724 dvlemap 12745 dvaddxxbr 12761 dvmulxxbr 12762 dvcoapbr 12767 dvcjbr 12768 dvrecap 12773 dveflem 12782 |
Copyright terms: Public domain | W3C validator |