Theorem rspc 3611

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

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1535   = wceq 1537  Ⅎwnf 1784   ∈ wcel 2114  ∀wral 3138

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-v 3496

This theorem is referenced by:  rspcvOLD  3619  rspc2  3631  rspc2vd  3932  disjxiun  5063  pofun  5491  fmptcof  6892  fliftfuns  7067  ofmpteq  7428  qliftfuns  8384  xpf1o  8679  iunfi  8812  iundom2g  9962  lble  11593  rlimcld2  14935  sumeq2ii  15050  summolem3  15071  zsum  15075  fsum  15077  fsumf1o  15080  sumss2  15083  fsumcvg2  15084  fsumadd  15096  isummulc2  15117  fsum2dlem  15125  fsumcom2  15129  fsumshftm  15136  fsum0diag2  15138  fsummulc2  15139  fsum00  15153  fsumabs  15156  fsumrelem  15162  fsumrlim  15166  fsumo1  15167  o1fsum  15168  fsumiun  15176  isumshft  15194  prodeq2ii  15267  prodmolem3  15287  zprod  15291  fprod  15295  fprodf1o  15300  prodss  15301  fprodser  15303  fprodmul  15314  fproddiv  15315  fprodm1s  15324  fprodp1s  15325  fprodabs  15328  fprod2dlem  15334  fprodcom2  15338  fprodefsum  15448  sumeven  15738  sumodd  15739  pcmpt  16228  invfuc  17244  dprd2d2  19166  txcnp  22228  ptcnplem  22229  prdsdsf  22977  prdsxmet  22979  fsumcn  23478  ovolfiniun  24102  ovoliunnul  24108  volfiniun  24148  iunmbl  24154  limciun  24492  dvfsumle  24618  dvfsumabs  24620  dvfsumlem1  24623  dvfsumlem3  24625  dvfsumlem4  24626  dvfsumrlim  24628  dvfsumrlim2  24629  dvfsum2  24631  itgsubst  24646  fsumvma  25789  dchrisumlema  26064  dchrisumlem2  26066  dchrisumlem3  26067  chirred  30172  fsumiunle  30545  sigapildsyslem  31420  voliune  31488  volfiniune  31489  tfisg  33055  nosupbnd1  33214  ptrest  34906  poimirlem25  34932  poimirlem26  34933  mzpsubst  39365  rabdiophlem2  39419  etransclem48  42587  sge0iunmpt  42720  2reu8i  43332