![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > rgen | GIF version |
Description: Generalization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.) |
Ref | Expression |
---|---|
rgen.1 | ⊢ (𝑥 ∈ 𝐴 → 𝜑) |
Ref | Expression |
---|---|
rgen | ⊢ ∀𝑥 ∈ 𝐴 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ral 2473 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
2 | rgen.1 | . 2 ⊢ (𝑥 ∈ 𝐴 → 𝜑) | |
3 | 1, 2 | mpgbir 1464 | 1 ⊢ ∀𝑥 ∈ 𝐴 𝜑 |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2160 ∀wral 2468 |
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 1460 |
This theorem depends on definitions: df-bi 117 df-ral 2473 |
This theorem is referenced by: rgen2a 2544 rgenw 2545 mprg 2547 mprgbir 2548 rgen2 2576 r19.21be 2581 nrex 2582 rexlimi 2600 sbcth2 3065 reuss 3431 ral0 3539 unimax 3858 mpteq1 4102 mpteq2ia 4104 ordon 4503 tfis 4600 finds 4617 finds2 4618 ordom 4624 omsinds 4639 dmxpid 4866 fnopab 5359 fmpti 5688 opabex3 6146 oawordriexmid 6494 fifo 7008 inresflem 7088 0ct 7135 infnninf 7151 infnninfOLD 7152 exmidonfinlem 7221 pw1on 7254 netap 7282 2omotaplemap 7285 indpi 7370 nnindnn 7921 aptap 8636 sup3exmid 8943 nnssre 8952 nnind 8964 nnsub 8987 dfuzi 9392 indstr 9622 cnref1o 9679 frec2uzsucd 10431 uzsinds 10472 ser0f 10545 bccl 10778 rexuz3 11030 isumlessdc 11535 prodf1f 11582 iprodap0 11621 eff2 11719 reeff1 11739 prmind2 12151 3prm 12159 sqrt2irr 12193 phisum 12271 pockthi 12389 1arith 12398 1arith2 12399 prminf 12505 xpsff1o 12822 rngmgpf 13288 mgpf 13362 cnfld1 13872 cnsubglem 13879 isbasis3g 13998 distop 14037 cdivcncfap 14539 dveflem 14639 ioocosf1o 14727 2irrexpqap 14848 2sqlem6 14920 2sqlem10 14925 bj-indint 15136 bj-nnelirr 15158 bj-omord 15165 012of 15199 2o01f 15200 0nninf 15207 nconstwlpolem0 15265 |
Copyright terms: Public domain | W3C validator |