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

Theorem rspc 2704
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 2358 . 2 (∀𝑥𝐵 𝜑 ↔ ∀𝑥(𝑥𝐵𝜑))
2 nfcv 2223 . . . 4 𝑥𝐴
3 nfv 1462 . . . . 5 𝑥 𝐴𝐵
4 rspc.1 . . . . 5 𝑥𝜓
53, 4nfim 1505 . . . 4 𝑥(𝐴𝐵𝜓)
6 eleq1 2145 . . . . 5 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
7 rspc.2 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
86, 7imbi12d 232 . . . 4 (𝑥 = 𝐴 → ((𝑥𝐵𝜑) ↔ (𝐴𝐵𝜓)))
92, 5, 8spcgf 2689 . . 3 (𝐴𝐵 → (∀𝑥(𝑥𝐵𝜑) → (𝐴𝐵𝜓)))
109pm2.43a 50 . 2 (𝐴𝐵 → (∀𝑥(𝑥𝐵𝜑) → 𝜓))
111, 10syl5bi 150 1 (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103  wal 1283   = wceq 1285  wnf 1390  wcel 1434  wral 2353
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065
This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ral 2358  df-v 2612
This theorem is referenced by:  rspcv  2706  rspc2  2719  pofun  4095  fmptcof  5384  fliftfuns  5490  qliftfuns  6278  xpf1o  6407  ssfirab  6476  lble  8162  exfzdc  9396  uzsinds  9588  sumeq2d  10415  sumeq2  10416  zsupcllemstep  10566  infssuzex  10570  bezoutlemmain  10612  bj-nntrans  11031
  Copyright terms: Public domain W3C validator