Theorem rspc 3609

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

Step	Hyp	Ref	Expression
1		df-ral 3059	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
2		nfcv 2902	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfv 1911	. . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
4		rspc.1	. . . . 5 ⊢ Ⅎ𝑥𝜓
5	3, 4	nfim 1893	. . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓)
6		eleq1 2826	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
7		rspc.2	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
8	6, 7	imbi12d 344	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))
9	2, 5, 8	spcgf 3590	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → (𝐴 ∈ 𝐵 → 𝜓)))
10	9	pm2.43a 54	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → 𝜓))
11	1, 10	biimtrid 242	1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1534   = wceq 1536  Ⅎwnf 1779   ∈ wcel 2105  ∀wral 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1776  df-nf 1780  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059

This theorem is referenced by:  rspc2  3630  rspc2vd  3958  disjxiun  5144  pofun  5614  fmptcof  7149  fliftfuns  7333  ofmpteq  7719  tfisg  7874  qliftfuns  8842  xpf1o  9177  iunfi  9380  iundom2g  10577  lble  12217  rlimcld2  15610  sumeq2ii  15725  summolem3  15746  zsum  15750  fsum  15752  fsumf1o  15755  sumss2  15758  fsumcvg2  15759  fsumadd  15772  isummulc2  15794  fsum2dlem  15802  fsumcom2  15806  fsumshftm  15813  fsum0diag2  15815  fsummulc2  15816  fsum00  15830  fsumabs  15833  fsumrelem  15839  fsumrlim  15843  fsumo1  15844  o1fsum  15845  fsumiun  15853  isumshft  15871  prodeq2ii  15943  prodmolem3  15965  zprod  15969  fprod  15973  fprodf1o  15978  prodss  15979  fprodser  15981  fprodmul  15992  fproddiv  15993  fprodm1s  16002  fprodp1s  16003  fprodabs  16006  fprod2dlem  16012  fprodcom2  16016  fprodefsum  16127  sumeven  16420  sumodd  16421  pcmpt  16925  invfuc  18030  dprd2d2  20078  txcnp  23643  ptcnplem  23644  prdsdsf  24392  prdsxmet  24394  fsumcn  24907  ovolfiniun  25549  ovoliunnul  25555  volfiniun  25595  iunmbl  25601  limciun  25943  dvfsumle  26074  dvfsumleOLD  26075  dvfsumabs  26077  dvfsumlem1  26080  dvfsumlem3  26083  dvfsumlem4  26084  dvfsumrlim  26086  dvfsumrlim2  26087  dvfsum2  26089  itgsubst  26104  fsumvma  27271  dchrisumlema  27546  dchrisumlem2  27548  dchrisumlem3  27549  nosupbnd1  27773  noinfbnd1  27788  chirred  32423  fsumiunle  32835  sigapildsyslem  34141  voliune  34209  volfiniune  34210  ptrest  37605  poimirlem25  37631  poimirlem26  37632  mzpsubst  42735  rabdiophlem2  42789  cvgcaule  45441  etransclem48  46237  sge0iunmpt  46373  2reu8i  47062