![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rspcdv | Structured version Visualization version GIF version |
Description: Restricted specialization, using implicit substitution. (Contributed by NM, 17-Feb-2007.) (Revised by Mario Carneiro, 4-Jan-2017.) |
Ref | Expression |
---|---|
rspcdv.1 | ⊢ (𝜑 → 𝐴 ∈ 𝐵) |
rspcdv.2 | ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
rspcdv | ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 → 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rspcdv.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵) | |
2 | rspcdv.2 | . . 3 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) | |
3 | 2 | biimpd 228 | . 2 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒)) |
4 | 1, 3 | rspcimdv 3598 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 → 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 = wceq 1534 ∈ wcel 2099 ∀wral 3051 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-ral 3052 |
This theorem is referenced by: rspcdv2 3603 rspcv 3604 ralxfrd 5403 ralxfrd2 5407 reuop 6295 suppofss1d 8209 suppofss2d 8210 zindd 12707 wrd2ind 14724 ismri2dad 17643 mreexd 17648 mreexexlemd 17650 catcocl 17691 catass 17692 moni 17745 subccocl 17857 funcco 17883 fullfo 17927 fthf1 17932 nati 17971 mndind 18811 ringurd 20162 idsrngd 20829 mpomulcn 24871 fsumdvdsmul 27218 uspgr2wlkeq 29578 crctcshwlkn0lem4 29742 crctcshwlkn0lem5 29743 wwlknllvtx 29775 0enwwlksnge1 29793 wlkiswwlks2lem5 29802 clwlkclwwlklem2a 29926 clwlkclwwlklem2 29928 clwwisshclwws 29943 clwwlkinwwlk 29968 umgr2cwwk2dif 29992 wrdt2ind 32818 mgccole1 32861 mgccole2 32862 mgcmnt1 32863 mgcmntco 32865 dfmgc2lem 32866 chnind 32881 1arithufdlem3 33425 dfufd2 33429 fedgmullem2 33529 constrconj 33615 zart0 33705 zarcmplem 33707 esumcvg 33930 inelcarsg 34156 carsgclctunlem1 34162 orvcelel 34314 signsply0 34408 onint1 36172 qsalrel 41984 ismnushort 44010 ralbinrald 46769 fargshiftfva 47049 reupr 47128 evengpop3 47404 evengpoap3 47405 snlindsntorlem 47887 |
Copyright terms: Public domain | W3C validator |