Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  rspcimdv Structured version   Visualization version   GIF version

Theorem rspcimdv 3438
 Description: Restricted specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.)
Hypotheses
Ref Expression
rspcimdv.1 (𝜑𝐴𝐵)
rspcimdv.2 ((𝜑𝑥 = 𝐴) → (𝜓𝜒))
Assertion
Ref Expression
rspcimdv (𝜑 → (∀𝑥𝐵 𝜓𝜒))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜑,𝑥   𝜒,𝑥
Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem rspcimdv
StepHypRef Expression
1 df-ral 3043 . 2 (∀𝑥𝐵 𝜓 ↔ ∀𝑥(𝑥𝐵𝜓))
2 rspcimdv.1 . . 3 (𝜑𝐴𝐵)
3 simpr 479 . . . . . . 7 ((𝜑𝑥 = 𝐴) → 𝑥 = 𝐴)
43eleq1d 2812 . . . . . 6 ((𝜑𝑥 = 𝐴) → (𝑥𝐵𝐴𝐵))
54biimprd 238 . . . . 5 ((𝜑𝑥 = 𝐴) → (𝐴𝐵𝑥𝐵))
6 rspcimdv.2 . . . . 5 ((𝜑𝑥 = 𝐴) → (𝜓𝜒))
75, 6imim12d 81 . . . 4 ((𝜑𝑥 = 𝐴) → ((𝑥𝐵𝜓) → (𝐴𝐵𝜒)))
82, 7spcimdv 3418 . . 3 (𝜑 → (∀𝑥(𝑥𝐵𝜓) → (𝐴𝐵𝜒)))
92, 8mpid 44 . 2 (𝜑 → (∀𝑥(𝑥𝐵𝜓) → 𝜒))
101, 9syl5bi 232 1 (𝜑 → (∀𝑥𝐵 𝜓𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383  ∀wal 1618   = wceq 1620   ∈ wcel 2127  ∀wral 3038 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ral 3043  df-v 3330 This theorem is referenced by:  rspcimedv  3439  rspcdv  3440  wrd2ind  13648  mreexd  16475  mreexexlemd  16477  catcocl  16518  catass  16519  moni  16568  subccocl  16677  funcco  16703  fullfo  16744  fthf1  16749  nati  16787  acsfiindd  17349  chpscmat  20820  friendshipgt3  27537  lmxrge0  30278  funressnfv  41683
 Copyright terms: Public domain W3C validator