ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  rspc GIF version

Theorem rspc 2730
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 2375 . 2 (∀𝑥𝐵 𝜑 ↔ ∀𝑥(𝑥𝐵𝜑))
2 nfcv 2235 . . . 4 𝑥𝐴
3 nfv 1473 . . . . 5 𝑥 𝐴𝐵
4 rspc.1 . . . . 5 𝑥𝜓
53, 4nfim 1516 . . . 4 𝑥(𝐴𝐵𝜓)
6 eleq1 2157 . . . . 5 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
7 rspc.2 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
86, 7imbi12d 233 . . . 4 (𝑥 = 𝐴 → ((𝑥𝐵𝜑) ↔ (𝐴𝐵𝜓)))
92, 5, 8spcgf 2715 . . 3 (𝐴𝐵 → (∀𝑥(𝑥𝐵𝜑) → (𝐴𝐵𝜓)))
109pm2.43a 51 . 2 (𝐴𝐵 → (∀𝑥(𝑥𝐵𝜑) → 𝜓))
111, 10syl5bi 151 1 (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104  wal 1294   = wceq 1296  wnf 1401  wcel 1445  wral 2370
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077
This theorem depends on definitions:  df-bi 116  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-ral 2375  df-v 2635
This theorem is referenced by:  rspcv  2732  rspc2  2746  pofun  4163  omsinds  4463  fmptcof  5504  fliftfuns  5615  qliftfuns  6416  xpf1o  6640  finexdc  6698  ssfirab  6723  iunfidisj  6735  lble  8505  exfzdc  9800  uzsinds  9997  sumeq2  10902  sumfct  10917  sumrbdclem  10919  summodclem3  10923  summodclem2a  10924  zsumdc  10927  fsumgcl  10929  fsum3  10930  fsumf1o  10933  isumss  10934  isumss2  10936  fsum3cvg2  10937  fsumadd  10949  isummulc2  10969  fsum2dlemstep  10977  fisumcom2  10981  fsumshftm  10988  fisum0diag2  10990  fsummulc2  10991  fsum00  11005  fsumabs  11008  fsumrelem  11014  fsumiun  11020  isumshft  11033  mertenslem2  11079  zsupcllemstep  11368  infssuzex  11372  bezoutlemmain  11414  iuncld  11967  bj-nntrans  12554
  Copyright terms: Public domain W3C validator