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

Theorem rspc 3554
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 3063 . 2 (∀𝑥𝐵 𝜑 ↔ ∀𝑥(𝑥𝐵𝜑))
2 nfcv 2905 . . . 4 𝑥𝐴
3 nfv 1915 . . . . 5 𝑥 𝐴𝐵
4 rspc.1 . . . . 5 𝑥𝜓
53, 4nfim 1897 . . . 4 𝑥(𝐴𝐵𝜓)
6 eleq1 2824 . . . . 5 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
7 rspc.2 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
86, 7imbi12d 345 . . . 4 (𝑥 = 𝐴 → ((𝑥𝐵𝜑) ↔ (𝐴𝐵𝜓)))
92, 5, 8spcgf 3535 . . 3 (𝐴𝐵 → (∀𝑥(𝑥𝐵𝜑) → (𝐴𝐵𝜓)))
109pm2.43a 54 . 2 (𝐴𝐵 → (∀𝑥(𝑥𝐵𝜑) → 𝜓))
111, 10biimtrid 241 1 (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1537   = wceq 1539  wnf 1783  wcel 2104  wral 3062
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-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-tru 1542  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ral 3063  df-v 3439
This theorem is referenced by:  rspc2  3573  rspc2vd  3888  disjxiun  5078  pofun  5532  fmptcof  7034  fliftfuns  7217  ofmpteq  7587  qliftfuns  8624  xpf1o  8964  iunfi  9155  iundom2g  10346  lble  11977  rlimcld2  15336  sumeq2ii  15454  summolem3  15475  zsum  15479  fsum  15481  fsumf1o  15484  sumss2  15487  fsumcvg2  15488  fsumadd  15501  isummulc2  15523  fsum2dlem  15531  fsumcom2  15535  fsumshftm  15542  fsum0diag2  15544  fsummulc2  15545  fsum00  15559  fsumabs  15562  fsumrelem  15568  fsumrlim  15572  fsumo1  15573  o1fsum  15574  fsumiun  15582  isumshft  15600  prodeq2ii  15672  prodmolem3  15692  zprod  15696  fprod  15700  fprodf1o  15705  prodss  15706  fprodser  15708  fprodmul  15719  fproddiv  15720  fprodm1s  15729  fprodp1s  15730  fprodabs  15733  fprod2dlem  15739  fprodcom2  15743  fprodefsum  15853  sumeven  16145  sumodd  16146  pcmpt  16642  invfuc  17741  dprd2d2  19696  txcnp  22820  ptcnplem  22821  prdsdsf  23569  prdsxmet  23571  fsumcn  24082  ovolfiniun  24714  ovoliunnul  24720  volfiniun  24760  iunmbl  24766  limciun  25107  dvfsumle  25234  dvfsumabs  25236  dvfsumlem1  25239  dvfsumlem3  25241  dvfsumlem4  25242  dvfsumrlim  25244  dvfsumrlim2  25245  dvfsum2  25247  itgsubst  25262  fsumvma  26410  dchrisumlema  26685  dchrisumlem2  26687  dchrisumlem3  26688  chirred  30806  fsumiunle  31192  sigapildsyslem  32178  voliune  32246  volfiniune  32247  tfisg  33835  nosupbnd1  33966  noinfbnd1  33981  ptrest  35824  poimirlem25  35850  poimirlem26  35851  mzpsubst  40765  rabdiophlem2  40819  etransclem48  44052  sge0iunmpt  44186  2reu8i  44849
  Copyright terms: Public domain W3C validator