Theorem rspc 3559

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 3111	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
2		nfcv 2955	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfv 1915	. . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
4		rspc.1	. . . . 5 ⊢ Ⅎ𝑥𝜓
5	3, 4	nfim 1897	. . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓)
6		eleq1 2877	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
7		rspc.2	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
8	6, 7	imbi12d 348	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))
9	2, 5, 8	spcgf 3538	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → (𝐴 ∈ 𝐵 → 𝜓)))
10	9	pm2.43a 54	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → 𝜓))
11	1, 10	syl5bi 245	1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1536   = wceq 1538  Ⅎwnf 1785   ∈ wcel 2111  ∀wral 3106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-v 3443

This theorem is referenced by:  rspcvOLD  3567  rspc2  3579  rspc2vd  3877  disjxiun  5027  pofun  5455  fmptcof  6869  fliftfuns  7046  ofmpteq  7408  qliftfuns  8367  xpf1o  8663  iunfi  8796  iundom2g  9951  lble  11580  rlimcld2  14927  sumeq2ii  15042  summolem3  15063  zsum  15067  fsum  15069  fsumf1o  15072  sumss2  15075  fsumcvg2  15076  fsumadd  15088  isummulc2  15109  fsum2dlem  15117  fsumcom2  15121  fsumshftm  15128  fsum0diag2  15130  fsummulc2  15131  fsum00  15145  fsumabs  15148  fsumrelem  15154  fsumrlim  15158  fsumo1  15159  o1fsum  15160  fsumiun  15168  isumshft  15186  prodeq2ii  15259  prodmolem3  15279  zprod  15283  fprod  15287  fprodf1o  15292  prodss  15293  fprodser  15295  fprodmul  15306  fproddiv  15307  fprodm1s  15316  fprodp1s  15317  fprodabs  15320  fprod2dlem  15326  fprodcom2  15330  fprodefsum  15440  sumeven  15728  sumodd  15729  pcmpt  16218  invfuc  17236  dprd2d2  19159  txcnp  22225  ptcnplem  22226  prdsdsf  22974  prdsxmet  22976  fsumcn  23475  ovolfiniun  24105  ovoliunnul  24111  volfiniun  24151  iunmbl  24157  limciun  24497  dvfsumle  24624  dvfsumabs  24626  dvfsumlem1  24629  dvfsumlem3  24631  dvfsumlem4  24632  dvfsumrlim  24634  dvfsumrlim2  24635  dvfsum2  24637  itgsubst  24652  fsumvma  25797  dchrisumlema  26072  dchrisumlem2  26074  dchrisumlem3  26075  chirred  30178  fsumiunle  30571  sigapildsyslem  31530  voliune  31598  volfiniune  31599  tfisg  33168  nosupbnd1  33327  ptrest  35056  poimirlem25  35082  poimirlem26  35083  mzpsubst  39689  rabdiophlem2  39743  etransclem48  42924  sge0iunmpt  43057  2reu8i  43669