![]() |
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 2530 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-gen 1449 |
This theorem depends on definitions: df-bi 117 df-ral 2460 |
This theorem is referenced by: rgen2w 2533 reuun1 3419 0disj 4002 iinexgm 4156 epse 4344 xpiindim 4766 eliunxp 4768 opeliunxp2 4769 elrnmpti 4882 fnmpti 5346 mpoeq12 5937 iunex 6126 mpoex 6217 opeliunxp2f 6241 ixpssmap 6734 1domsn 6821 nneneq 6859 nqprrnd 7544 nqprdisj 7545 uzf 9533 sum0 11398 fisumcom2 11448 prod0 11595 fprodcom2fi 11636 phisum 12242 sumhashdc 12347 unennn 12400 tgidm 13659 tgrest 13754 txbas 13843 reldvg 14233 dvfvalap 14235 bj-indint 14768 bj-nn0suc0 14787 bj-nntrans 14788 |
Copyright terms: Public domain | W3C validator |