Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > rabbidva | Unicode version |
Description: Equivalent wff's yield equal restricted class abstractions (deduction form). (Contributed by NM, 28-Nov-2003.) |
Ref | Expression |
---|---|
rabbidva.1 |
Ref | Expression |
---|---|
rabbidva |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rabbidva.1 | . . 3 | |
2 | 1 | ralrimiva 2543 | . 2 |
3 | rabbi 2647 | . 2 | |
4 | 2, 3 | sylib 121 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wb 104 wceq 1348 wcel 2141 wral 2448 crab 2452 |
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 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-11 1499 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-tru 1351 df-nf 1454 df-sb 1756 df-clab 2157 df-cleq 2163 df-ral 2453 df-rab 2457 |
This theorem is referenced by: rabbidv 2719 rabeqbidva 2726 rabbi2dva 3335 rabxfrd 4452 onsucmin 4489 seinxp 4680 fniniseg2 5616 fnniniseg2 5617 f1oresrab 5659 dfinfre 8865 minmax 11186 xrminmax 11221 iooinsup 11233 gcdass 11963 lcmass 12032 pcneg 12271 bdbl 13262 xmetxpbl 13267 |
Copyright terms: Public domain | W3C validator |