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

Theorem rspc 2757
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 2398 . 2 (∀𝑥𝐵 𝜑 ↔ ∀𝑥(𝑥𝐵𝜑))
2 nfcv 2258 . . . 4 𝑥𝐴
3 nfv 1493 . . . . 5 𝑥 𝐴𝐵
4 rspc.1 . . . . 5 𝑥𝜓
53, 4nfim 1536 . . . 4 𝑥(𝐴𝐵𝜓)
6 eleq1 2180 . . . . 5 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
7 rspc.2 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
86, 7imbi12d 233 . . . 4 (𝑥 = 𝐴 → ((𝑥𝐵𝜑) ↔ (𝐴𝐵𝜓)))
92, 5, 8spcgf 2742 . . 3 (𝐴𝐵 → (∀𝑥(𝑥𝐵𝜑) → (𝐴𝐵𝜓)))
109pm2.43a 51 . 2 (𝐴𝐵 → (∀𝑥(𝑥𝐵𝜑) → 𝜓))
111, 10syl5bi 151 1 (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104  wal 1314   = wceq 1316  wnf 1421  wcel 1465  wral 2393
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-ral 2398  df-v 2662
This theorem is referenced by:  rspcv  2759  rspc2  2774  pofun  4204  omsinds  4505  fmptcof  5555  fliftfuns  5667  qliftfuns  6481  xpf1o  6706  finexdc  6764  ssfirab  6790  iunfidisj  6802  lble  8673  exfzdc  9985  uzsinds  10183  sumeq2  11096  sumfct  11111  sumrbdclem  11113  summodclem3  11117  summodclem2a  11118  zsumdc  11121  fsumgcl  11123  fsum3  11124  fsumf1o  11127  isumss  11128  isumss2  11130  fsum3cvg2  11131  fsumadd  11143  isummulc2  11163  fsum2dlemstep  11171  fisumcom2  11175  fsumshftm  11182  fisum0diag2  11184  fsummulc2  11185  fsum00  11199  fsumabs  11202  fsumrelem  11208  fsumiun  11214  isumshft  11227  mertenslem2  11273  zsupcllemstep  11565  infssuzex  11569  bezoutlemmain  11613  ctiunctlemudc  11877  iuncld  12211  txcnp  12367  fsumcncntop  12652  bj-nntrans  13076
  Copyright terms: Public domain W3C validator