![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > rgenw | GIF 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: ∈ wcel 2148 ∀wral 2455 |
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 3417 0disj 4000 iinexgm 4154 epse 4342 xpiindim 4764 eliunxp 4766 opeliunxp2 4767 elrnmpti 4880 fnmpti 5344 mpoeq12 5934 iunex 6123 mpoex 6214 opeliunxp2f 6238 ixpssmap 6731 1domsn 6818 nneneq 6856 nqprrnd 7541 nqprdisj 7542 uzf 9530 sum0 11395 fisumcom2 11445 prod0 11592 fprodcom2fi 11633 phisum 12239 sumhashdc 12344 unennn 12397 tgidm 13510 tgrest 13605 txbas 13694 reldvg 14084 dvfvalap 14086 bj-indint 14619 bj-nn0suc0 14638 bj-nntrans 14639 |
Copyright terms: Public domain | W3C validator |