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 1508 | . 2 ⊢ Ⅎ𝑥𝜓 | |
2 | rspcv.1 | . 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
3 | 1, 2 | rspc 2778 | 1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 = wceq 1331 ∈ wcel 1480 ∀wral 2414 |
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 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2119 |
This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2124 df-cleq 2130 df-clel 2133 df-nfc 2268 df-ral 2419 df-v 2683 |
This theorem is referenced by: rspccv 2781 rspcva 2782 rspccva 2783 rspcdva 2789 rspc3v 2800 rr19.3v 2818 rr19.28v 2819 rspsbc 2986 intmin 3786 ralxfrALT 4383 ontr2exmid 4435 reg2exmidlema 4444 0elsucexmid 4475 funcnvuni 5187 acexmidlemcase 5762 tfrlem1 6198 tfrlem9 6209 oawordriexmid 6359 nneneq 6744 diffitest 6774 xpfi 6811 ordiso2 6913 prnmaxl 7289 prnminu 7290 cauappcvgprlemm 7446 cauappcvgprlemladdru 7457 cauappcvgprlemladdrl 7458 caucvgsrlemcl 7590 caucvgsrlemfv 7592 caucvgsr 7603 axcaucvglemres 7700 lbreu 8696 nnsub 8752 supinfneg 9383 infsupneg 9384 ublbneg 9398 fzrevral 9878 seq3caopr3 10247 seq3id3 10273 recan 10874 cau3lem 10879 caubnd2 10882 climshftlemg 11064 subcn2 11073 climcau 11109 serf0 11114 sumdc 11120 isumrpcl 11256 clim2prod 11301 ndvdssub 11616 zsupcllemex 11628 dfgcd3 11687 dfgcd2 11691 coprmgcdb 11758 coprmdvds1 11761 nprm 11793 dvdsprm 11806 coprm 11811 sqrt2irr 11829 cnpnei 12377 lmss 12404 txlm 12437 psmet0 12485 metss 12652 metcnp3 12669 mulc1cncf 12734 cncfco 12736 bj-indsuc 13115 bj-inf2vnlem2 13158 |
Copyright terms: Public domain | W3C validator |