![]() |
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 230 | . 2 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒)) |
4 | 1, 3 | rspcimdv 3562 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 → 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1525 ∈ wcel 2083 ∀wral 3107 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-ext 2771 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1766 df-sb 2045 df-clab 2778 df-cleq 2790 df-clel 2865 df-ral 3112 df-v 3442 |
This theorem is referenced by: ralxfrd 5207 ralxfrd2 5211 reuop 6026 suppofss1d 7726 suppofss2d 7727 zindd 11937 wrd2ind 13925 ismri2dad 16741 mreexd 16746 mreexexlemd 16748 catcocl 16789 catass 16790 moni 16839 subccocl 16948 funcco 16974 fullfo 17015 fthf1 17020 nati 17058 mndind 17809 idsrngd 19327 uspgr2wlkeq 27114 crctcshwlkn0lem4 27277 crctcshwlkn0lem5 27278 wwlknllvtx 27310 0enwwlksnge1 27328 wlkiswwlks2lem5 27337 clwlkclwwlklem2a 27462 clwlkclwwlklem2 27464 clwwisshclwws 27479 clwwlkinwwlk 27504 umgr2cwwk2dif 27529 wrdt2ind 30302 rngurd 30507 fedgmullem2 30626 esumcvg 30958 inelcarsg 31182 carsgclctunlem1 31188 orvcelel 31340 signsply0 31434 onint1 33408 qsalrel 38676 rspcdvinvd 40031 ralbinrald 42859 fargshiftfva 43107 reupr 43188 evengpop3 43467 evengpoap3 43468 isomgrsym 43505 snlindsntorlem 44027 |
Copyright terms: Public domain | W3C validator |