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 2398 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
2 | rgen.1 | . 2 ⊢ (𝑥 ∈ 𝐴 → 𝜑) | |
3 | 1, 2 | mpgbir 1414 | 1 ⊢ ∀𝑥 ∈ 𝐴 𝜑 |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1465 ∀wral 2393 |
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 1410 |
This theorem depends on definitions: df-bi 116 df-ral 2398 |
This theorem is referenced by: rgen2a 2463 rgenw 2464 mprg 2466 mprgbir 2467 rgen2 2495 r19.21be 2500 nrex 2501 rexlimi 2519 sbcth2 2968 reuss 3327 ral0 3434 unimax 3740 mpteq1 3982 mpteq2ia 3984 ordon 4372 tfis 4467 finds 4484 finds2 4485 ordom 4490 omsinds 4505 dmxpid 4730 fnopab 5217 fmpti 5540 opabex3 5988 oawordriexmid 6334 fifo 6836 inresflem 6913 0ct 6960 infnninf 6990 exmidonfinlem 7017 indpi 7118 nnindnn 7669 sup3exmid 8683 nnssre 8692 nnind 8704 nnsub 8727 dfuzi 9129 indstr 9356 cnref1o 9408 frec2uzsucd 10142 uzsinds 10183 ser0f 10256 bccl 10481 rexuz3 10730 isumlessdc 11233 eff2 11313 reeff1 11334 prmind2 11728 3prm 11736 sqrt2irr 11767 isbasis3g 12140 distop 12181 cdivcncfap 12683 dveflem 12782 bj-indint 13056 bj-nnelirr 13078 bj-omord 13085 0nninf 13124 isomninnlem 13152 |
Copyright terms: Public domain | W3C validator |