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 3127 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝑥 ∈ 𝐴 → 𝜑)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝑥 ∈ 𝐴 → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2110 ∀wral 3061 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-12 2175 |
This theorem depends on definitions: df-bi 210 df-ex 1788 df-ral 3066 |
This theorem is referenced by: rspec2 3132 vtoclri 3501 wfis 6206 wfis2f 6208 wfis2 6210 isarep2 6469 mpoexw 7849 ecopover 8503 frins 9368 alephsuc2 9694 indstr 12512 reltxrnmnf 12932 ackbijnn 15392 mrelatglb0 18067 0frgp 19169 iccpnfcnv 23841 prter2 36632 |
Copyright terms: Public domain | W3C validator |