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 2913 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝑥 ∈ 𝐴 → 𝜑)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝑥 ∈ 𝐴 → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 1977 ∀wral 2896 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-12 2034 |
This theorem depends on definitions: df-bi 196 df-ex 1696 df-ral 2901 |
This theorem is referenced by: rspec2 2918 vtoclri 3256 wfis 5633 wfis2f 5635 wfis2 5637 isarep2 5892 ecopover 7738 ecopoverOLD 7739 alephsuc2 8786 indstr 11632 reltxrnmnf 12043 ackbijnn 14399 mrelatglb0 17008 0frgp 18015 iccpnfcnv 22551 frins 30987 frins2f 30989 prter2 33184 |
Copyright terms: Public domain | W3C validator |