Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > rspcv | GIF version |
Description: Restricted specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) |
Ref | Expression |
---|---|
rspcv.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
rspcv | ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1515 | . 2 ⊢ Ⅎ𝑥𝜓 | |
2 | rspcv.1 | . 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
3 | 1, 2 | rspc 2819 | 1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 = wceq 1342 ∈ wcel 2135 ∀wral 2442 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-10 1492 ax-11 1493 ax-i12 1494 ax-bndl 1496 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-tru 1345 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-nfc 2295 df-ral 2447 df-v 2723 |
This theorem is referenced by: rspccv 2822 rspcva 2823 rspccva 2824 rspcdva 2830 rspc3v 2841 rr19.3v 2860 rr19.28v 2861 rspsbc 3028 intmin 3838 ralxfrALT 4439 ontr2exmid 4496 reg2exmidlema 4505 0elsucexmid 4536 funcnvuni 5251 acexmidlemcase 5831 tfrlem1 6267 tfrlem9 6278 oawordriexmid 6429 nneneq 6814 diffitest 6844 xpfi 6886 ordiso2 6991 exmidontriimlem3 7170 prnmaxl 7420 prnminu 7421 cauappcvgprlemm 7577 cauappcvgprlemladdru 7588 cauappcvgprlemladdrl 7589 caucvgsrlemcl 7721 caucvgsrlemfv 7723 caucvgsr 7734 axcaucvglemres 7831 lbreu 8831 nnsub 8887 supinfneg 9524 infsupneg 9525 ublbneg 9542 fzrevral 10030 seq3caopr3 10406 seq3id3 10432 recan 11037 cau3lem 11042 caubnd2 11045 climshftlemg 11229 subcn2 11238 climcau 11274 serf0 11279 sumdc 11285 isumrpcl 11421 clim2prod 11466 prodmodclem2 11504 ndvdssub 11852 zsupcllemex 11864 dfgcd3 11928 dfgcd2 11932 coprmgcdb 11999 coprmdvds1 12002 nprm 12034 dvdsprm 12048 coprm 12053 sqrt2irr 12071 pcmpt 12250 pcmptdvds 12252 pcfac 12257 cnpnei 12760 lmss 12787 txlm 12820 psmet0 12868 metss 13035 metcnp3 13052 mulc1cncf 13117 cncfco 13119 bj-indsuc 13645 bj-inf2vnlem2 13688 trirec0 13757 iswomni0 13764 |
Copyright terms: Public domain | W3C validator |