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

Theorem rspc 3276
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 2901 . 2 (∀𝑥𝐵 𝜑 ↔ ∀𝑥(𝑥𝐵𝜑))
2 nfcv 2751 . . . 4 𝑥𝐴
3 nfv 1830 . . . . 5 𝑥 𝐴𝐵
4 rspc.1 . . . . 5 𝑥𝜓
53, 4nfim 1813 . . . 4 𝑥(𝐴𝐵𝜓)
6 eleq1 2676 . . . . 5 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
7 rspc.2 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
86, 7imbi12d 333 . . . 4 (𝑥 = 𝐴 → ((𝑥𝐵𝜑) ↔ (𝐴𝐵𝜓)))
92, 5, 8spcgf 3261 . . 3 (𝐴𝐵 → (∀𝑥(𝑥𝐵𝜑) → (𝐴𝐵𝜓)))
109pm2.43a 52 . 2 (𝐴𝐵 → (∀𝑥(𝑥𝐵𝜑) → 𝜓))
111, 10syl5bi 231 1 (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wal 1473   = wceq 1475  wnf 1699  wcel 1977  wral 2896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-v 3175
This theorem is referenced by:  rspcv  3278  rspc2  3292  disjxiun  4574  disjxiunOLD  4575  pofun  4965  fmptcof  6289  fliftfuns  6442  ofmpteq  6792  qliftfuns  7699  xpf1o  7985  iunfi  8115  iundom2g  9219  lble  10827  rlimcld2  14106  sumeq2ii  14220  summolem3  14241  zsum  14245  fsum  14247  fsumf1o  14250  sumss2  14253  fsumcvg2  14254  fsumadd  14266  isummulc2  14284  fsum2dlem  14292  fsumcom2  14296  fsumcom2OLD  14297  fsumshftm  14304  fsum0diag2  14306  fsummulc2  14307  fsum00  14320  fsumabs  14323  fsumrelem  14329  fsumrlim  14333  fsumo1  14334  o1fsum  14335  fsumiun  14343  isumshft  14359  prodeq2ii  14431  prodmolem3  14451  zprod  14455  fprod  14459  fprodf1o  14464  prodss  14465  fprodser  14467  fprodmul  14478  fproddiv  14479  fprodm1s  14488  fprodp1s  14489  fprodabs  14492  fprod2dlem  14498  fprodcom2  14502  fprodcom2OLD  14503  fprodefsum  14613  sumeven  14897  sumodd  14898  pcmpt  15383  invfuc  16406  dprd2d2  18215  txcnp  21181  ptcnplem  21182  prdsdsf  21930  prdsxmet  21932  fsumcn  22429  ovolfiniun  23021  ovoliunnul  23027  volfiniun  23067  iunmbl  23073  limciun  23409  dvfsumle  23533  dvfsumabs  23535  dvfsumlem1  23538  dvfsumlem3  23540  dvfsumlem4  23541  dvfsumrlim  23543  dvfsumrlim2  23544  dvfsum2  23546  itgsubst  23561  fsumvma  24683  dchrisumlema  24922  dchrisumlem2  24924  dchrisumlem3  24925  chirred  28432  sigapildsyslem  29345  voliune  29413  volfiniune  29414  tfisg  30754  ptrest  32372  poimirlem25  32398  poimirlem26  32399  mzpsubst  36123  rabdiophlem2  36178  etransclem48  38969  sge0iunmpt  39105  rspc2vd  41429
  Copyright terms: Public domain W3C validator