Theorem rspc 3539

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 3068	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
2		nfcv 2906	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfv 1918	. . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
4		rspc.1	. . . . 5 ⊢ Ⅎ𝑥𝜓
5	3, 4	nfim 1900	. . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓)
6		eleq1 2826	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
7		rspc.2	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
8	6, 7	imbi12d 344	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))
9	2, 5, 8	spcgf 3520	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → (𝐴 ∈ 𝐵 → 𝜓)))
10	9	pm2.43a 54	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → 𝜓))
11	1, 10	syl5bi 241	1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537   = wceq 1539  Ⅎwnf 1787   ∈ wcel 2108  ∀wral 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-v 3424

This theorem is referenced by:  rspcvOLD  3548  rspc2  3560  rspc2vd  3879  disjxiun  5067  pofun  5512  fmptcof  6984  fliftfuns  7165  ofmpteq  7533  qliftfuns  8551  xpf1o  8875  iunfi  9037  iundom2g  10227  lble  11857  rlimcld2  15215  sumeq2ii  15333  summolem3  15354  zsum  15358  fsum  15360  fsumf1o  15363  sumss2  15366  fsumcvg2  15367  fsumadd  15380  isummulc2  15402  fsum2dlem  15410  fsumcom2  15414  fsumshftm  15421  fsum0diag2  15423  fsummulc2  15424  fsum00  15438  fsumabs  15441  fsumrelem  15447  fsumrlim  15451  fsumo1  15452  o1fsum  15453  fsumiun  15461  isumshft  15479  prodeq2ii  15551  prodmolem3  15571  zprod  15575  fprod  15579  fprodf1o  15584  prodss  15585  fprodser  15587  fprodmul  15598  fproddiv  15599  fprodm1s  15608  fprodp1s  15609  fprodabs  15612  fprod2dlem  15618  fprodcom2  15622  fprodefsum  15732  sumeven  16024  sumodd  16025  pcmpt  16521  invfuc  17608  dprd2d2  19562  txcnp  22679  ptcnplem  22680  prdsdsf  23428  prdsxmet  23430  fsumcn  23939  ovolfiniun  24570  ovoliunnul  24576  volfiniun  24616  iunmbl  24622  limciun  24963  dvfsumle  25090  dvfsumabs  25092  dvfsumlem1  25095  dvfsumlem3  25097  dvfsumlem4  25098  dvfsumrlim  25100  dvfsumrlim2  25101  dvfsum2  25103  itgsubst  25118  fsumvma  26266  dchrisumlema  26541  dchrisumlem2  26543  dchrisumlem3  26544  chirred  30658  fsumiunle  31045  sigapildsyslem  32029  voliune  32097  volfiniune  32098  tfisg  33692  nosupbnd1  33844  noinfbnd1  33859  ptrest  35703  poimirlem25  35729  poimirlem26  35730  mzpsubst  40486  rabdiophlem2  40540  etransclem48  43713  sge0iunmpt  43846  2reu8i  44492