![]() |
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 3155 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝑥 ∈ 𝐴 → 𝜑)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝑥 ∈ 𝐴 → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2050 ∀wral 3088 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-12 2106 |
This theorem depends on definitions: df-bi 199 df-ex 1743 df-ral 3093 |
This theorem is referenced by: rspec2 3161 vtoclri 3504 wfis 6024 wfis2f 6026 wfis2 6028 isarep2 6278 mpoexw 7586 ecopover 8203 alephsuc2 9302 indstr 12133 reltxrnmnf 12554 ackbijnn 15046 mrelatglb0 17656 0frgp 18668 iccpnfcnv 23254 frins 32609 frins2f 32611 prter2 35462 |
Copyright terms: Public domain | W3C validator |