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

Theorem rspcimdv 3601
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 3060 . 2 (∀𝑥𝐵 𝜓 ↔ ∀𝑥(𝑥𝐵𝜓))
2 rspcimdv.1 . . 3 (𝜑𝐴𝐵)
3 simpr 483 . . . . . . 7 ((𝜑𝑥 = 𝐴) → 𝑥 = 𝐴)
43eleq1d 2816 . . . . . 6 ((𝜑𝑥 = 𝐴) → (𝑥𝐵𝐴𝐵))
54biimprd 247 . . . . 5 ((𝜑𝑥 = 𝐴) → (𝐴𝐵𝑥𝐵))
6 rspcimdv.2 . . . . 5 ((𝜑𝑥 = 𝐴) → (𝜓𝜒))
75, 6imim12d 81 . . . 4 ((𝜑𝑥 = 𝐴) → ((𝑥𝐵𝜓) → (𝐴𝐵𝜒)))
82, 7spcimdv 3582 . . 3 (𝜑 → (∀𝑥(𝑥𝐵𝜓) → (𝐴𝐵𝜒)))
92, 8mpid 44 . 2 (𝜑 → (∀𝑥(𝑥𝐵𝜓) → 𝜒))
101, 9biimtrid 241 1 (𝜑 → (∀𝑥𝐵 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  wal 1537   = wceq 1539  wcel 2104  wral 3059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ral 3060
This theorem is referenced by:  rspcimedv  3602  rspcdv  3603  wrd2ind  14677  mreexd  17590  mreexexlemd  17592  catcocl  17633  catass  17634  moni  17687  subccocl  17799  funcco  17825  fullfo  17867  fthf1  17872  nati  17910  acsfiindd  18510  chpscmat  22564  mpomulcn  24605  friendshipgt3  29918  lmxrge0  33230  funressnfv  46051  cfsetsnfsetf1  46067
  Copyright terms: Public domain W3C validator