Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > elab2 | Unicode version |
Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.) |
Ref | Expression |
---|---|
elab2.1 | |
elab2.2 | |
elab2.3 |
Ref | Expression |
---|---|
elab2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elab2.1 | . 2 | |
2 | elab2.2 | . . 3 | |
3 | elab2.3 | . . 3 | |
4 | 2, 3 | elab2g 2873 | . 2 |
5 | 1, 4 | ax-mp 5 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 wceq 1343 wcel 2136 cab 2151 cvv 2726 |
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-io 699 ax-5 1435 ax-7 1436 ax-gen 1437 ax-ie1 1481 ax-ie2 1482 ax-8 1492 ax-10 1493 ax-11 1494 ax-i12 1495 ax-bndl 1497 ax-4 1498 ax-17 1514 ax-i9 1518 ax-ial 1522 ax-i5r 1523 ax-ext 2147 |
This theorem depends on definitions: df-bi 116 df-tru 1346 df-nf 1449 df-sb 1751 df-clab 2152 df-cleq 2158 df-clel 2161 df-nfc 2297 df-v 2728 |
This theorem is referenced by: elpw 3565 elint 3830 opabid 4235 elrn2 4846 elimasn 4971 oprabid 5874 tfrlem3a 6278 tfrcllemsucaccv 6322 tfrcllembxssdm 6324 tfrcllemres 6330 addnqprlemrl 7498 addnqprlemru 7499 addnqprlemfl 7500 addnqprlemfu 7501 mulnqprlemrl 7514 mulnqprlemru 7515 mulnqprlemfl 7516 mulnqprlemfu 7517 ltnqpr 7534 ltnqpri 7535 archpr 7584 cauappcvgprlemladdfu 7595 cauappcvgprlemladdfl 7596 caucvgprlemladdfu 7618 caucvgprprlemopu 7640 suplocexprlemloc 7662 txuni2 12896 |
Copyright terms: Public domain | W3C validator |