Theorem rspc 3334

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 2946	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
2		nfcv 2793	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfv 1883	. . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
4		rspc.1	. . . . 5 ⊢ Ⅎ𝑥𝜓
5	3, 4	nfim 1865	. . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓)
6		eleq1 2718	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
7		rspc.2	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
8	6, 7	imbi12d 333	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))
9	2, 5, 8	spcgf 3319	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → (𝐴 ∈ 𝐵 → 𝜓)))
10	9	pm2.43a 54	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → 𝜓))
11	1, 10	syl5bi 232	1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 196  ∀wal 1521   = wceq 1523  Ⅎwnf 1748   ∈ wcel 2030  ∀wral 2941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-v 3233

This theorem is referenced by:  rspcv  3336  rspc2  3351  disjxiun  4681  disjxiunOLD  4682  pofun  5080  fmptcof  6437  fliftfuns  6604  ofmpteq  6958  qliftfuns  7877  xpf1o  8163  iunfi  8295  iundom2g  9400  lble  11013  rlimcld2  14353  sumeq2ii  14467  summolem3  14489  zsum  14493  fsum  14495  fsumf1o  14498  sumss2  14501  fsumcvg2  14502  fsumadd  14514  isummulc2  14537  fsum2dlem  14545  fsumcom2  14549  fsumcom2OLD  14550  fsumshftm  14557  fsum0diag2  14559  fsummulc2  14560  fsum00  14574  fsumabs  14577  fsumrelem  14583  fsumrlim  14587  fsumo1  14588  o1fsum  14589  fsumiun  14597  isumshft  14615  prodeq2ii  14687  prodmolem3  14707  zprod  14711  fprod  14715  fprodf1o  14720  prodss  14721  fprodser  14723  fprodmul  14734  fproddiv  14735  fprodm1s  14744  fprodp1s  14745  fprodabs  14748  fprod2dlem  14754  fprodcom2  14758  fprodcom2OLD  14759  fprodefsum  14869  sumeven  15157  sumodd  15158  pcmpt  15643  invfuc  16681  dprd2d2  18489  txcnp  21471  ptcnplem  21472  prdsdsf  22219  prdsxmet  22221  fsumcn  22720  ovolfiniun  23315  ovoliunnul  23321  volfiniun  23361  iunmbl  23367  limciun  23703  dvfsumle  23829  dvfsumabs  23831  dvfsumlem1  23834  dvfsumlem3  23836  dvfsumlem4  23837  dvfsumrlim  23839  dvfsumrlim2  23840  dvfsum2  23842  itgsubst  23857  fsumvma  24983  dchrisumlema  25222  dchrisumlem2  25224  dchrisumlem3  25225  rspc2vd  27245  chirred  29382  fsumiunle  29703  sigapildsyslem  30352  voliune  30420  volfiniune  30421  tfisg  31840  nosupbnd1  31985  ptrest  33538  poimirlem25  33564  poimirlem26  33565  mzpsubst  37628  rabdiophlem2  37683  etransclem48  40817  sge0iunmpt  40953