|   | 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 229 | . 2 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒)) | 
| 4 | 1, 3 | rspcimdv 3611 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 → 𝜒)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1539 ∈ wcel 2107 ∀wral 3060 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1542 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-ral 3061 | 
| This theorem is referenced by: rspcdv2 3616 rspcv 3617 ralxfrd 5407 ralxfrd2 5411 reuop 6312 suppofss1d 8230 suppofss2d 8231 zindd 12721 wrd2ind 14762 ismri2dad 17681 mreexd 17686 mreexexlemd 17688 catcocl 17729 catass 17730 moni 17781 subccocl 17891 funcco 17917 fullfo 17960 fthf1 17965 nati 18004 mndind 18842 ringurd 20183 idsrngd 20858 mpomulcn 24892 fsumdvdsmul 27239 uspgr2wlkeq 29665 crctcshwlkn0lem4 29834 crctcshwlkn0lem5 29835 wwlknllvtx 29867 0enwwlksnge1 29885 wlkiswwlks2lem5 29894 clwlkclwwlklem2a 30018 clwlkclwwlklem2 30020 clwwisshclwws 30035 clwwlkinwwlk 30060 umgr2cwwk2dif 30084 wrdt2ind 32939 mgccole1 32981 mgccole2 32982 mgcmnt1 32983 mgcmntco 32985 dfmgc2lem 32986 chnind 33002 1arithufdlem3 33575 dfufd2 33579 fedgmullem2 33682 constrconj 33787 zart0 33879 zarcmplem 33881 esumcvg 34088 inelcarsg 34314 carsgclctunlem1 34320 orvcelel 34473 signsply0 34567 onint1 36451 qsalrel 42281 ismnushort 44325 ralbinrald 47139 fargshiftfva 47435 reupr 47514 evengpop3 47790 evengpoap3 47791 snlindsntorlem 48392 | 
| Copyright terms: Public domain | W3C validator |