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 2453 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
2 | rgen.1 | . 2 ⊢ (𝑥 ∈ 𝐴 → 𝜑) | |
3 | 1, 2 | mpgbir 1446 | 1 ⊢ ∀𝑥 ∈ 𝐴 𝜑 |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2141 ∀wral 2448 |
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 1442 |
This theorem depends on definitions: df-bi 116 df-ral 2453 |
This theorem is referenced by: rgen2a 2524 rgenw 2525 mprg 2527 mprgbir 2528 rgen2 2556 r19.21be 2561 nrex 2562 rexlimi 2580 sbcth2 3042 reuss 3408 ral0 3515 unimax 3828 mpteq1 4071 mpteq2ia 4073 ordon 4468 tfis 4565 finds 4582 finds2 4583 ordom 4589 omsinds 4604 dmxpid 4830 fnopab 5320 fmpti 5646 opabex3 6099 oawordriexmid 6447 fifo 6954 inresflem 7034 0ct 7081 infnninf 7097 infnninfOLD 7098 exmidonfinlem 7159 pw1on 7192 indpi 7293 nnindnn 7844 sup3exmid 8862 nnssre 8871 nnind 8883 nnsub 8906 dfuzi 9311 indstr 9541 cnref1o 9598 frec2uzsucd 10346 uzsinds 10387 ser0f 10460 bccl 10690 rexuz3 10943 isumlessdc 11448 prodf1f 11495 iprodap0 11534 eff2 11632 reeff1 11652 prmind2 12063 3prm 12071 sqrt2irr 12105 phisum 12183 pockthi 12299 1arith 12308 1arith2 12309 prminf 12399 isbasis3g 12799 distop 12840 cdivcncfap 13342 dveflem 13442 ioocosf1o 13530 2irrexpqap 13651 2sqlem6 13711 2sqlem10 13716 bj-indint 13928 bj-nnelirr 13950 bj-omord 13957 012of 13990 2o01f 13991 0nninf 13999 nconstwlpolem0 14056 |
Copyright terms: Public domain | W3C validator |