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 3202 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝑥 ∈ 𝐴 → 𝜑)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝑥 ∈ 𝐴 → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2105 ∀wral 3135 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-12 2167 |
This theorem depends on definitions: df-bi 208 df-ex 1772 df-ral 3140 |
This theorem is referenced by: rspec2 3208 vtoclri 3582 wfis 6177 wfis2f 6179 wfis2 6181 isarep2 6436 mpoexw 7765 ecopover 8390 alephsuc2 9494 indstr 12304 reltxrnmnf 12723 ackbijnn 15171 mrelatglb0 17783 0frgp 18834 iccpnfcnv 23475 frins 32985 frins2f 32987 prter2 35897 |
Copyright terms: Public domain | W3C validator |