Theorem rspc 3276

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 2901	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
2		nfcv 2751	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfv 1830	. . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
4		rspc.1	. . . . 5 ⊢ Ⅎ𝑥𝜓
5	3, 4	nfim 1813	. . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓)
6		eleq1 2676	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
7		rspc.2	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
8	6, 7	imbi12d 333	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))
9	2, 5, 8	spcgf 3261	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → (𝐴 ∈ 𝐵 → 𝜓)))
10	9	pm2.43a 52	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → 𝜓))
11	1, 10	syl5bi 231	1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 195  ∀wal 1473   = wceq 1475  Ⅎwnf 1699   ∈ wcel 1977  ∀wral 2896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-v 3175

This theorem is referenced by:  rspcv  3278  rspc2  3292  disjxiun  4579  disjxiunOLD  4580  pofun  4975  fmptcof  6304  fliftfuns  6464  ofmpteq  6814  qliftfuns  7721  xpf1o  8007  iunfi  8137  iundom2g  9241  lble  10854  rlimcld2  14157  sumeq2ii  14271  summolem3  14292  zsum  14296  fsum  14298  fsumf1o  14301  sumss2  14304  fsumcvg2  14305  fsumadd  14317  isummulc2  14335  fsum2dlem  14343  fsumcom2  14347  fsumcom2OLD  14348  fsumshftm  14355  fsum0diag2  14357  fsummulc2  14358  fsum00  14371  fsumabs  14374  fsumrelem  14380  fsumrlim  14384  fsumo1  14385  o1fsum  14386  fsumiun  14394  isumshft  14410  prodeq2ii  14482  prodmolem3  14502  zprod  14506  fprod  14510  fprodf1o  14515  prodss  14516  fprodser  14518  fprodmul  14529  fproddiv  14530  fprodm1s  14539  fprodp1s  14540  fprodabs  14543  fprod2dlem  14549  fprodcom2  14553  fprodcom2OLD  14554  fprodefsum  14664  sumeven  14948  sumodd  14949  pcmpt  15434  invfuc  16457  dprd2d2  18266  txcnp  21233  ptcnplem  21234  prdsdsf  21982  prdsxmet  21984  fsumcn  22481  ovolfiniun  23076  ovoliunnul  23082  volfiniun  23122  iunmbl  23128  limciun  23464  dvfsumle  23588  dvfsumabs  23590  dvfsumlem1  23593  dvfsumlem3  23595  dvfsumlem4  23596  dvfsumrlim  23598  dvfsumrlim2  23599  dvfsum2  23601  itgsubst  23616  fsumvma  24738  dchrisumlema  24977  dchrisumlem2  24979  dchrisumlem3  24980  chirred  28638  sigapildsyslem  29551  voliune  29619  volfiniune  29620  tfisg  30960  ptrest  32578  poimirlem25  32604  poimirlem26  32605  mzpsubst  36329  rabdiophlem2  36384  etransclem48  39175  sge0iunmpt  39311  rspc2vd  41437