New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > rgen | GIF version |
Description: Generalization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.) |
Ref | Expression |
---|---|
rgen.1 | ⊢ (x ∈ A → φ) |
Ref | Expression |
---|---|
rgen | ⊢ ∀x ∈ A φ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ral 2619 | . 2 ⊢ (∀x ∈ A φ ↔ ∀x(x ∈ A → φ)) | |
2 | rgen.1 | . 2 ⊢ (x ∈ A → φ) | |
3 | 1, 2 | mpgbir 1550 | 1 ⊢ ∀x ∈ A φ |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 1710 ∀wral 2614 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 |
This theorem depends on definitions: df-bi 177 df-ral 2619 |
This theorem is referenced by: rgen2a 2680 rgenw 2681 mprg 2683 mprgbir 2684 rgen2 2710 r19.21be 2715 nrex 2716 rexlimi 2731 sbcth2 3129 reuss 3536 r19.2zb 3640 ral0 3654 unimax 3925 nndisjeq 4429 fnopab 5207 mpteq1 5658 mpteq2ia 5659 fmpti 5693 clos1is 5881 nclenn 6249 nmembers1lem2 6269 nnc3n3p1 6278 nchoicelem12 6300 |
Copyright terms: Public domain | W3C validator |