![]() |
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 2459 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-gen 1408 |
This theorem depends on definitions: df-bi 116 df-ral 2395 |
This theorem is referenced by: rgen2w 2462 reuun1 3324 0disj 3892 iinexgm 4039 epse 4224 xpiindim 4636 eliunxp 4638 opeliunxp2 4639 elrnmpti 4752 fnmpti 5209 mpoeq12 5785 iunex 5975 mpoex 6065 opeliunxp2f 6089 ixpssmap 6580 1domsn 6666 nneneq 6704 nqprrnd 7299 nqprdisj 7300 uzf 9231 sum0 11049 fisumcom2 11099 unennn 11755 tgidm 12086 tgrest 12181 txbas 12269 reldvg 12603 dvfvalap 12605 bj-indint 12821 bj-nn0suc0 12840 bj-nntrans 12841 |
Copyright terms: Public domain | W3C validator |