Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > rspec | Structured version Visualization version Unicode 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 2929 | . 2 | |
3 | 1, 2 | ax-mp 5 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wcel 1990 wral 2912 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-12 2047 |
This theorem depends on definitions: df-bi 197 df-ex 1705 df-ral 2917 |
This theorem is referenced by: rspec2 2934 vtoclri 3283 wfis 5716 wfis2f 5718 wfis2 5720 isarep2 5978 ecopover 7851 ecopoverOLD 7852 alephsuc2 8903 indstr 11756 reltxrnmnf 12172 ackbijnn 14560 mrelatglb0 17185 0frgp 18192 iccpnfcnv 22743 frins 31743 frins2f 31745 prter2 34166 |
Copyright terms: Public domain | W3C validator |