Theorem rspc 3568

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 3081	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
2		nfcv 2926	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfv 1949	. . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
4		rspc.1	. . . . 5 ⊢ Ⅎ𝑥𝜓
5	3, 4	nfim 1931	. . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓)
6		eleq1 2852	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
7		rspc.2	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
8	6, 7	imbi12d 347	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))
9	2, 5, 8	spcgf 3549	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → (𝐴 ∈ 𝐵 → 𝜓)))
10	9	pm2.43a 55	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → 𝜓))
11	1, 10	biimtrid 245	1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568   = wceq 1570  Ⅎwnf 1816   ∈ wcel 2147  ∀wral 3080

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-nf 1817  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081

This theorem is used by:  rspc2  3588  rspc2vd  3899  disjxiun  5103  pofun  5581  fmptcof  7155  fliftfuns  7345  ofmpteq  7740  tfisg  7889  qliftfuns  8853  xpf1o  9186  iunfi  9360  iundom2g  10651  lble  12296  rlimcld2  15774  sumeq2ii  15889  summolem3  15909  zsum  15913  fsum  15915  fsumf1o  15918  sumss2  15921  fsumcvg2  15922  fsumadd  15935  isummulc2  15957  fsum2dlem  15965  fsumcom2  15969  fsumshftm  15976  fsum0diag2  15978  fsummulc2  15979  fsum00  15994  fsumabs  15997  fsumrelem  16003  fsumrlim  16007  fsumo1  16008  o1fsum  16009  fsumiun  16017  isumshft  16037  prodeq2ii  16109  prodmolem3  16129  zprod  16133  fprod  16137  fprodf1o  16142  prodss  16143  fprodser  16145  fprodmul  16156  fproddiv  16157  fprodm1s  16166  fprodp1s  16167  fprodabs  16170  fprod2dlem  16176  fprodcom2  16180  fprodefsum  16290  sumeven  16586  sumodd  16587  pcmpt  17099  invfuc  18181  dprd2d2  20290  txcnp  23969  ptcnplem  23970  prdsdsf  24716  prdsxmet  24718  fsumcn  25221  ovolfiniun  25852  ovoliunnul  25858  volfiniun  25898  iunmbl  25904  limciun  26244  dvfsumle  26371  dvfsumabs  26373  dvfsumlem1  26376  dvfsumlem3  26378  dvfsumlem4  26379  dvfsumrlim  26381  dvfsumrlim2  26382  dvfsum2  26384  itgsubst  26399  fsumvma  27570  dchrisumlema  27845  dchrisumlem2  27847  dchrisumlem3  27848  nosupbnd1  28101  noinfbnd1  28116  chirred  33027  fsumiunle  33490  sigapildsyslem  34864  voliune  34932  volfiniune  34933  ptrest  38729  poimirlem25  38755  poimirlem26  38756  mzpsubst  43952  rabdiophlem2  44002  cvgcaule  46706  etransclem48  47497  sge0iunmpt  47633  2reu8i  48389