![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rspec | Structured version Visualization version GIF version |
Description: Specialization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.) |
Ref | Expression |
---|---|
rspec.1 | ⊢ ∀𝑥 ∈ 𝐴 𝜑 |
Ref | Expression |
---|---|
rspec | ⊢ (𝑥 ∈ 𝐴 → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rspec.1 | . 2 ⊢ ∀𝑥 ∈ 𝐴 𝜑 | |
2 | rsp 3244 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝑥 ∈ 𝐴 → 𝜑)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝑥 ∈ 𝐴 → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2106 ∀wral 3061 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-12 2171 |
This theorem depends on definitions: df-bi 206 df-ex 1782 df-ral 3062 |
This theorem is referenced by: rspec2 3276 vtoclri 3576 wfis 6353 wfis2f 6356 wfis2 6358 isarep2 6636 mpoexw 8061 ecopover 8811 frins 9743 alephsuc2 10071 indstr 12896 reltxrnmnf 13317 ackbijnn 15770 mrelatglb0 18510 0frgp 19641 iccpnfcnv 24451 prter2 37739 natlocalincr 45576 natglobalincr 45577 |
Copyright terms: Public domain | W3C validator |