![]() |
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 219 | . 2 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒)) |
4 | 1, 3 | rspcimdv 3450 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 → 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 = wceq 1632 ∈ wcel 2139 ∀wral 3050 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-clab 2747 df-cleq 2753 df-clel 2756 df-nfc 2891 df-ral 3055 df-v 3342 |
This theorem is referenced by: ralxfrd 5028 ralxfrdOLD 5029 ralxfrd2 5033 suppofss1d 7501 suppofss2d 7502 zindd 11670 wrd2ind 13677 ismri2dad 16499 mreexd 16504 mreexexlemd 16506 catcocl 16547 catass 16548 moni 16597 subccocl 16706 funcco 16732 fullfo 16773 fthf1 16778 nati 16816 mrcmndind 17567 idsrngd 19064 flfcntr 22048 uspgr2wlkeq 26752 crctcshwlkn0lem4 26916 crctcshwlkn0lem5 26917 wwlknllvtx 26950 0enwwlksnge1 26973 wlkiswwlks2lem5 26982 clwlkclwwlklem2a 27121 clwlkclwwlklem2 27123 clwwisshclwws 27138 clwwlkinwwlk 27169 umgr2cwwk2dif 27195 rngurd 30097 esumcvg 30457 inelcarsg 30682 carsgclctunlem1 30688 orvcelel 30840 signsply0 30937 onint1 32754 rspcdvinvd 38976 ralbinrald 41705 fargshiftfva 41889 evengpop3 42196 evengpoap3 42197 snlindsntorlem 42769 |
Copyright terms: Public domain | W3C validator |