![]() |
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 1489 | . 2 ⊢ Ⅎ𝑥𝜓 | |
2 | rspcv.1 | . 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
3 | 1, 2 | rspc 2752 | 1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 = wceq 1312 ∈ wcel 1461 ∀wral 2388 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 681 ax-5 1404 ax-7 1405 ax-gen 1406 ax-ie1 1450 ax-ie2 1451 ax-8 1463 ax-10 1464 ax-11 1465 ax-i12 1466 ax-bndl 1467 ax-4 1468 ax-17 1487 ax-i9 1491 ax-ial 1495 ax-i5r 1496 ax-ext 2095 |
This theorem depends on definitions: df-bi 116 df-tru 1315 df-nf 1418 df-sb 1717 df-clab 2100 df-cleq 2106 df-clel 2109 df-nfc 2242 df-ral 2393 df-v 2657 |
This theorem is referenced by: rspccv 2755 rspcva 2756 rspccva 2757 rspcdva 2763 rspc3v 2773 rr19.3v 2791 rr19.28v 2792 rspsbc 2957 intmin 3755 ralxfrALT 4346 ontr2exmid 4398 reg2exmidlema 4407 0elsucexmid 4438 funcnvuni 5148 acexmidlemcase 5721 tfrlem1 6156 tfrlem9 6167 oawordriexmid 6317 nneneq 6701 diffitest 6731 xpfi 6768 ordiso2 6869 prnmaxl 7237 prnminu 7238 cauappcvgprlemm 7394 cauappcvgprlemladdru 7405 cauappcvgprlemladdrl 7406 caucvgsrlemcl 7524 caucvgsrlemfv 7526 caucvgsr 7537 axcaucvglemres 7627 lbreu 8606 nnsub 8662 supinfneg 9285 infsupneg 9286 ublbneg 9300 fzrevral 9771 seq3caopr3 10140 seq3id3 10166 recan 10766 cau3lem 10771 caubnd2 10774 climshftlemg 10956 subcn2 10965 climcau 11001 serf0 11006 sumdc 11012 isumrpcl 11148 ndvdssub 11468 zsupcllemex 11480 dfgcd3 11537 dfgcd2 11541 coprmgcdb 11608 coprmdvds1 11611 nprm 11643 dvdsprm 11656 coprm 11661 sqrt2irr 11679 cnpnei 12223 lmss 12250 txlm 12283 psmet0 12309 metss 12476 metcnp3 12493 mulc1cncf 12555 cncfco 12557 bj-indsuc 12805 bj-inf2vnlem2 12848 |
Copyright terms: Public domain | W3C validator |