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

Theorem rspc 3456
Description: Restricted specialization, using implicit substitution. (Contributed by NM, 19-Apr-2005.) (Revised by Mario Carneiro, 11-Oct-2016.)
Hypotheses
Ref Expression
rspc.1 𝑥𝜓
rspc.2 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
rspc (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)

Proof of Theorem rspc
StepHypRef Expression
1 df-ral 3060 . 2 (∀𝑥𝐵 𝜑 ↔ ∀𝑥(𝑥𝐵𝜑))
2 nfcv 2907 . . . 4 𝑥𝐴
3 nfv 2009 . . . . 5 𝑥 𝐴𝐵
4 rspc.1 . . . . 5 𝑥𝜓
53, 4nfim 1995 . . . 4 𝑥(𝐴𝐵𝜓)
6 eleq1 2832 . . . . 5 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
7 rspc.2 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
86, 7imbi12d 335 . . . 4 (𝑥 = 𝐴 → ((𝑥𝐵𝜑) ↔ (𝐴𝐵𝜓)))
92, 5, 8spcgf 3441 . . 3 (𝐴𝐵 → (∀𝑥(𝑥𝐵𝜑) → (𝐴𝐵𝜓)))
109pm2.43a 54 . 2 (𝐴𝐵 → (∀𝑥(𝑥𝐵𝜑) → 𝜓))
111, 10syl5bi 233 1 (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wal 1650   = wceq 1652  wnf 1878  wcel 2155  wral 3055
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ral 3060  df-v 3352
This theorem is referenced by:  rspcv  3458  rspc2  3473  disjxiun  4808  pofun  5216  fmptcof  6592  fliftfuns  6760  ofmpteq  7118  qliftfuns  8041  xpf1o  8333  iunfi  8465  iundom2g  9619  lble  11233  rlimcld2  14608  sumeq2ii  14722  summolem3  14744  zsum  14748  fsum  14750  fsumf1o  14753  sumss2  14756  fsumcvg2  14757  fsumadd  14769  isummulc2  14792  fsum2dlem  14800  fsumcom2  14804  fsumshftm  14811  fsum0diag2  14813  fsummulc2  14814  fsum00  14828  fsumabs  14831  fsumrelem  14837  fsumrlim  14841  fsumo1  14842  o1fsum  14843  fsumiun  14851  isumshft  14869  prodeq2ii  14940  prodmolem3  14960  zprod  14964  fprod  14968  fprodf1o  14973  prodss  14974  fprodser  14976  fprodmul  14987  fproddiv  14988  fprodm1s  14997  fprodp1s  14998  fprodabs  15001  fprod2dlem  15007  fprodcom2  15011  fprodefsum  15121  sumeven  15406  sumodd  15407  pcmpt  15889  invfuc  16913  dprd2d2  18724  txcnp  21717  ptcnplem  21718  prdsdsf  22465  prdsxmet  22467  fsumcn  22966  ovolfiniun  23573  ovoliunnul  23579  volfiniun  23619  iunmbl  23625  limciun  23963  dvfsumle  24089  dvfsumabs  24091  dvfsumlem1  24094  dvfsumlem3  24096  dvfsumlem4  24097  dvfsumrlim  24099  dvfsumrlim2  24100  dvfsum2  24102  itgsubst  24117  fsumvma  25243  dchrisumlema  25482  dchrisumlem2  25484  dchrisumlem3  25485  rspc2vd  27566  chirred  29731  fsumiunle  30045  sigapildsyslem  30692  voliune  30760  volfiniune  30761  tfisg  32180  nosupbnd1  32325  ptrest  33853  poimirlem25  33879  poimirlem26  33880  mzpsubst  38013  rabdiophlem2  38068  etransclem48  41160  sge0iunmpt  41296
  Copyright terms: Public domain W3C validator