![]() |
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 3603 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 → 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1542 ∈ wcel 2107 ∀wral 3062 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3063 |
This theorem is referenced by: rspcdv2 3608 rspcv 3609 ralxfrd 5407 ralxfrd2 5411 reuop 6293 suppofss1d 8189 suppofss2d 8190 zindd 12663 wrd2ind 14673 ismri2dad 17581 mreexd 17586 mreexexlemd 17588 catcocl 17629 catass 17630 moni 17683 subccocl 17795 funcco 17821 fullfo 17863 fthf1 17868 nati 17906 mndind 18709 ringurd 20008 idsrngd 20470 uspgr2wlkeq 28903 crctcshwlkn0lem4 29067 crctcshwlkn0lem5 29068 wwlknllvtx 29100 0enwwlksnge1 29118 wlkiswwlks2lem5 29127 clwlkclwwlklem2a 29251 clwlkclwwlklem2 29253 clwwisshclwws 29268 clwwlkinwwlk 29293 umgr2cwwk2dif 29317 wrdt2ind 32117 mgccole1 32160 mgccole2 32161 mgcmnt1 32162 mgcmntco 32164 dfmgc2lem 32165 fedgmullem2 32715 zart0 32859 zarcmplem 32861 esumcvg 33084 inelcarsg 33310 carsgclctunlem1 33316 orvcelel 33468 signsply0 33562 mpomulcn 35162 onint1 35334 qsalrel 41062 ismnushort 43060 ralbinrald 45830 fargshiftfva 46111 reupr 46190 evengpop3 46466 evengpoap3 46467 isomgrsym 46504 snlindsntorlem 47151 |
Copyright terms: Public domain | W3C validator |