Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > rgenw | Unicode version |
Description: Generalization rule for restricted quantification. (Contributed by NM, 18-Jun-2014.) |
Ref | Expression |
---|---|
rgenw.1 |
Ref | Expression |
---|---|
rgenw |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rgenw.1 | . . 3 | |
2 | 1 | a1i 9 | . 2 |
3 | 2 | rgen 2517 | 1 |
Colors of variables: wff set class |
Syntax hints: wcel 2135 wral 2442 |
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-gen 1436 |
This theorem depends on definitions: df-bi 116 df-ral 2447 |
This theorem is referenced by: rgen2w 2520 reuun1 3399 0disj 3973 iinexgm 4127 epse 4314 xpiindim 4735 eliunxp 4737 opeliunxp2 4738 elrnmpti 4851 fnmpti 5310 mpoeq12 5893 iunex 6083 mpoex 6173 opeliunxp2f 6197 ixpssmap 6689 1domsn 6776 nneneq 6814 nqprrnd 7475 nqprdisj 7476 uzf 9460 sum0 11315 fisumcom2 11365 prod0 11512 fprodcom2fi 11553 phisum 12151 sumhashdc 12256 unennn 12273 tgidm 12621 tgrest 12716 txbas 12805 reldvg 13195 dvfvalap 13197 bj-indint 13654 bj-nn0suc0 13673 bj-nntrans 13674 |
Copyright terms: Public domain | W3C validator |