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

Theorem rspcimdv 3561
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 3111 . 2 (∀𝑥𝐵 𝜓 ↔ ∀𝑥(𝑥𝐵𝜓))
2 rspcimdv.1 . . 3 (𝜑𝐴𝐵)
3 simpr 488 . . . . . . 7 ((𝜑𝑥 = 𝐴) → 𝑥 = 𝐴)
43eleq1d 2874 . . . . . 6 ((𝜑𝑥 = 𝐴) → (𝑥𝐵𝐴𝐵))
54biimprd 251 . . . . 5 ((𝜑𝑥 = 𝐴) → (𝐴𝐵𝑥𝐵))
6 rspcimdv.2 . . . . 5 ((𝜑𝑥 = 𝐴) → (𝜓𝜒))
75, 6imim12d 81 . . . 4 ((𝜑𝑥 = 𝐴) → ((𝑥𝐵𝜓) → (𝐴𝐵𝜒)))
82, 7spcimdv 3540 . . 3 (𝜑 → (∀𝑥(𝑥𝐵𝜓) → (𝐴𝐵𝜒)))
92, 8mpid 44 . 2 (𝜑 → (∀𝑥(𝑥𝐵𝜓) → 𝜒))
101, 9syl5bi 245 1 (𝜑 → (∀𝑥𝐵 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wal 1536   = wceq 1538  wcel 2111  wral 3106
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870  df-ral 3111
This theorem is referenced by:  rspcimedv  3562  rspcdv  3563  wrd2ind  14076  mreexd  16905  mreexexlemd  16907  catcocl  16948  catass  16949  moni  16998  subccocl  17107  funcco  17133  fullfo  17174  fthf1  17179  nati  17217  acsfiindd  17779  chpscmat  21447  friendshipgt3  28183  lmxrge0  31305  funressnfv  43633
  Copyright terms: Public domain W3C validator