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

Theorem rspcimdv 3603
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 3063 . 2 (∀𝑥𝐵 𝜓 ↔ ∀𝑥(𝑥𝐵𝜓))
2 rspcimdv.1 . . 3 (𝜑𝐴𝐵)
3 simpr 486 . . . . . . 7 ((𝜑𝑥 = 𝐴) → 𝑥 = 𝐴)
43eleq1d 2819 . . . . . 6 ((𝜑𝑥 = 𝐴) → (𝑥𝐵𝐴𝐵))
54biimprd 247 . . . . 5 ((𝜑𝑥 = 𝐴) → (𝐴𝐵𝑥𝐵))
6 rspcimdv.2 . . . . 5 ((𝜑𝑥 = 𝐴) → (𝜓𝜒))
75, 6imim12d 81 . . . 4 ((𝜑𝑥 = 𝐴) → ((𝑥𝐵𝜓) → (𝐴𝐵𝜒)))
82, 7spcimdv 3584 . . 3 (𝜑 → (∀𝑥(𝑥𝐵𝜓) → (𝐴𝐵𝜒)))
92, 8mpid 44 . 2 (𝜑 → (∀𝑥(𝑥𝐵𝜓) → 𝜒))
101, 9biimtrid 241 1 (𝜑 → (∀𝑥𝐵 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wal 1540   = 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:  rspcimedv  3604  rspcdv  3605  wrd2ind  14673  mreexd  17586  mreexexlemd  17588  catcocl  17629  catass  17630  moni  17683  subccocl  17795  funcco  17821  fullfo  17863  fthf1  17868  nati  17906  acsfiindd  18506  chpscmat  22344  friendshipgt3  29651  lmxrge0  32932  mpomulcn  35162  funressnfv  45753  cfsetsnfsetf1  45769
  Copyright terms: Public domain W3C validator