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 2544 | . 2 |
3 | rabbi 2648 | . 2 | |
4 | 2, 3 | sylib 121 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wb 104 wceq 1349 wcel 2142 wral 2449 crab 2453 |
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 1441 ax-7 1442 ax-gen 1443 ax-ie1 1487 ax-ie2 1488 ax-8 1498 ax-11 1500 ax-4 1504 ax-17 1520 ax-i9 1524 ax-ial 1528 ax-i5r 1529 ax-ext 2153 |
This theorem depends on definitions: df-bi 116 df-tru 1352 df-nf 1455 df-sb 1757 df-clab 2158 df-cleq 2164 df-ral 2454 df-rab 2458 |
This theorem is referenced by: rabbidv 2720 rabeqbidva 2727 rabbi2dva 3336 rabxfrd 4455 onsucmin 4492 seinxp 4683 fniniseg2 5622 fnniniseg2 5623 f1oresrab 5665 dfinfre 8876 minmax 11197 xrminmax 11232 iooinsup 11244 gcdass 11974 lcmass 12043 pcneg 12282 bdbl 13382 xmetxpbl 13387 |
Copyright terms: Public domain | W3C validator |