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

Theorem rspc 3615
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 3148 . 2 (∀𝑥𝐵 𝜑 ↔ ∀𝑥(𝑥𝐵𝜑))
2 nfcv 2982 . . . 4 𝑥𝐴
3 nfv 1908 . . . . 5 𝑥 𝐴𝐵
4 rspc.1 . . . . 5 𝑥𝜓
53, 4nfim 1890 . . . 4 𝑥(𝐴𝐵𝜓)
6 eleq1 2905 . . . . 5 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
7 rspc.2 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
86, 7imbi12d 346 . . . 4 (𝑥 = 𝐴 → ((𝑥𝐵𝜑) ↔ (𝐴𝐵𝜓)))
92, 5, 8spcgf 3595 . . 3 (𝐴𝐵 → (∀𝑥(𝑥𝐵𝜑) → (𝐴𝐵𝜓)))
109pm2.43a 54 . 2 (𝐴𝐵 → (∀𝑥(𝑥𝐵𝜑) → 𝜓))
111, 10syl5bi 243 1 (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wal 1528   = wceq 1530  wnf 1777  wcel 2107  wral 3143
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ral 3148  df-v 3502
This theorem is referenced by:  rspcvOLD  3623  rspc2  3635  rspc2vd  3936  disjxiun  5060  pofun  5490  fmptcof  6890  fliftfuns  7061  ofmpteq  7422  qliftfuns  8379  xpf1o  8673  iunfi  8806  iundom2g  9956  lble  11587  rlimcld2  14930  sumeq2ii  15045  summolem3  15066  zsum  15070  fsum  15072  fsumf1o  15075  sumss2  15078  fsumcvg2  15079  fsumadd  15091  isummulc2  15112  fsum2dlem  15120  fsumcom2  15124  fsumshftm  15131  fsum0diag2  15133  fsummulc2  15134  fsum00  15148  fsumabs  15151  fsumrelem  15157  fsumrlim  15161  fsumo1  15162  o1fsum  15163  fsumiun  15171  isumshft  15189  prodeq2ii  15262  prodmolem3  15282  zprod  15286  fprod  15290  fprodf1o  15295  prodss  15296  fprodser  15298  fprodmul  15309  fproddiv  15310  fprodm1s  15319  fprodp1s  15320  fprodabs  15323  fprod2dlem  15329  fprodcom2  15333  fprodefsum  15443  sumeven  15733  sumodd  15734  pcmpt  16223  invfuc  17239  dprd2d2  19102  txcnp  22163  ptcnplem  22164  prdsdsf  22911  prdsxmet  22913  fsumcn  23412  ovolfiniun  24036  ovoliunnul  24042  volfiniun  24082  iunmbl  24088  limciun  24426  dvfsumle  24552  dvfsumabs  24554  dvfsumlem1  24557  dvfsumlem3  24559  dvfsumlem4  24560  dvfsumrlim  24562  dvfsumrlim2  24563  dvfsum2  24565  itgsubst  24580  fsumvma  25722  dchrisumlema  25997  dchrisumlem2  25999  dchrisumlem3  26000  chirred  30105  fsumiunle  30478  sigapildsyslem  31325  voliune  31393  volfiniune  31394  tfisg  32958  nosupbnd1  33117  ptrest  34777  poimirlem25  34803  poimirlem26  34804  mzpsubst  39229  rabdiophlem2  39283  etransclem48  42452  sge0iunmpt  42585  2reu8i  43197
  Copyright terms: Public domain W3C validator