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

Theorem rspc 3540
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 3069 . 2 (∀𝑥𝐵 𝜑 ↔ ∀𝑥(𝑥𝐵𝜑))
2 nfcv 2907 . . . 4 𝑥𝐴
3 nfv 1922 . . . . 5 𝑥 𝐴𝐵
4 rspc.1 . . . . 5 𝑥𝜓
53, 4nfim 1904 . . . 4 𝑥(𝐴𝐵𝜓)
6 eleq1 2827 . . . . 5 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
7 rspc.2 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
86, 7imbi12d 348 . . . 4 (𝑥 = 𝐴 → ((𝑥𝐵𝜑) ↔ (𝐴𝐵𝜓)))
92, 5, 8spcgf 3521 . . 3 (𝐴𝐵 → (∀𝑥(𝑥𝐵𝜑) → (𝐴𝐵𝜓)))
109pm2.43a 54 . 2 (𝐴𝐵 → (∀𝑥(𝑥𝐵𝜑) → 𝜓))
111, 10syl5bi 245 1 (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wal 1541   = wceq 1543  wnf 1791  wcel 2112  wral 3064
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-nf 1792  df-sb 2073  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ral 3069  df-v 3425
This theorem is referenced by:  rspcvOLD  3548  rspc2  3560  rspc2vd  3879  disjxiun  5067  pofun  5504  fmptcof  6967  fliftfuns  7145  ofmpteq  7512  qliftfuns  8510  xpf1o  8834  iunfi  8994  iundom2g  10184  lble  11814  rlimcld2  15172  sumeq2ii  15290  summolem3  15311  zsum  15315  fsum  15317  fsumf1o  15320  sumss2  15323  fsumcvg2  15324  fsumadd  15337  isummulc2  15359  fsum2dlem  15367  fsumcom2  15371  fsumshftm  15378  fsum0diag2  15380  fsummulc2  15381  fsum00  15395  fsumabs  15398  fsumrelem  15404  fsumrlim  15408  fsumo1  15409  o1fsum  15410  fsumiun  15418  isumshft  15436  prodeq2ii  15508  prodmolem3  15528  zprod  15532  fprod  15536  fprodf1o  15541  prodss  15542  fprodser  15544  fprodmul  15555  fproddiv  15556  fprodm1s  15565  fprodp1s  15566  fprodabs  15569  fprod2dlem  15575  fprodcom2  15579  fprodefsum  15689  sumeven  15981  sumodd  15982  pcmpt  16478  invfuc  17516  dprd2d2  19464  txcnp  22549  ptcnplem  22550  prdsdsf  23297  prdsxmet  23299  fsumcn  23799  ovolfiniun  24430  ovoliunnul  24436  volfiniun  24476  iunmbl  24482  limciun  24823  dvfsumle  24950  dvfsumabs  24952  dvfsumlem1  24955  dvfsumlem3  24957  dvfsumlem4  24958  dvfsumrlim  24960  dvfsumrlim2  24961  dvfsum2  24963  itgsubst  24978  fsumvma  26126  dchrisumlema  26401  dchrisumlem2  26403  dchrisumlem3  26404  chirred  30508  fsumiunle  30895  sigapildsyslem  31873  voliune  31941  volfiniune  31942  tfisg  33536  nosupbnd1  33688  noinfbnd1  33703  ptrest  35550  poimirlem25  35576  poimirlem26  35577  mzpsubst  40321  rabdiophlem2  40375  etransclem48  43544  sge0iunmpt  43677  2reu8i  44323
  Copyright terms: Public domain W3C validator