![]() |
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 1539 | . 2 ⊢ Ⅎ𝑥𝜓 | |
2 | rspcv.1 | . 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
3 | 1, 2 | rspc 2850 | 1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 = wceq 1364 ∈ wcel 2160 ∀wral 2468 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ral 2473 df-v 2754 |
This theorem is referenced by: rspccv 2853 rspcva 2854 rspccva 2855 rspcdva 2861 rspc3v 2872 rr19.3v 2891 rr19.28v 2892 rspsbc 3060 rspc2vd 3140 intmin 3879 ralxfrALT 4485 ontr2exmid 4542 reg2exmidlema 4551 0elsucexmid 4582 funcnvuni 5304 acexmidlemcase 5892 tfrlem1 6334 tfrlem9 6345 oawordriexmid 6496 nneneq 6886 diffitest 6916 xpfi 6959 ordiso2 7065 exmidontriimlem3 7253 prnmaxl 7518 prnminu 7519 cauappcvgprlemm 7675 cauappcvgprlemladdru 7686 cauappcvgprlemladdrl 7687 caucvgsrlemcl 7819 caucvgsrlemfv 7821 caucvgsr 7832 axcaucvglemres 7929 lbreu 8933 nnsub 8989 supinfneg 9627 infsupneg 9628 ublbneg 9645 fzrevral 10137 seq3caopr3 10514 seq3id3 10540 recan 11153 cau3lem 11158 caubnd2 11161 climshftlemg 11345 subcn2 11354 climcau 11390 serf0 11395 sumdc 11401 isumrpcl 11537 clim2prod 11582 prodmodclem2 11620 ndvdssub 11970 zsupcllemex 11982 dfgcd3 12046 dfgcd2 12050 coprmgcdb 12123 coprmdvds1 12126 nprm 12158 dvdsprm 12172 coprm 12179 sqrt2irr 12197 pcmpt 12378 pcmptdvds 12380 pcfac 12385 prmpwdvds 12390 lidrididd 12861 dfgrp2 12986 grpidinv2 13017 dfgrp3mlem 13057 issubg4m 13149 srgrz 13355 srglz 13356 srgisid 13357 islmodd 13626 rmodislmod 13684 rnglidlmcl 13813 cnpnei 14196 lmss 14223 txlm 14256 psmet0 14304 metss 14471 metcnp3 14488 mulc1cncf 14553 cncfco 14555 2sqlem6 14945 2sqlem10 14950 bj-indsuc 15158 bj-inf2vnlem2 15201 trirec0 15271 iswomni0 15278 neap0mkv 15296 |
Copyright terms: Public domain | W3C validator |