Theorem rspc 3601

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1540   = wceq 1542  Ⅎwnf 1786   ∈ wcel 2107  ∀wral 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-v 3477

This theorem is referenced by:  rspc2  3621  rspc2vd  3945  disjxiun  5146  pofun  5607  fmptcof  7128  fliftfuns  7311  ofmpteq  7692  tfisg  7843  qliftfuns  8798  xpf1o  9139  iunfi  9340  iundom2g  10535  lble  12166  rlimcld2  15522  sumeq2ii  15639  summolem3  15660  zsum  15664  fsum  15666  fsumf1o  15669  sumss2  15672  fsumcvg2  15673  fsumadd  15686  isummulc2  15708  fsum2dlem  15716  fsumcom2  15720  fsumshftm  15727  fsum0diag2  15729  fsummulc2  15730  fsum00  15744  fsumabs  15747  fsumrelem  15753  fsumrlim  15757  fsumo1  15758  o1fsum  15759  fsumiun  15767  isumshft  15785  prodeq2ii  15857  prodmolem3  15877  zprod  15881  fprod  15885  fprodf1o  15890  prodss  15891  fprodser  15893  fprodmul  15904  fproddiv  15905  fprodm1s  15914  fprodp1s  15915  fprodabs  15918  fprod2dlem  15924  fprodcom2  15928  fprodefsum  16038  sumeven  16330  sumodd  16331  pcmpt  16825  invfuc  17927  dprd2d2  19914  txcnp  23124  ptcnplem  23125  prdsdsf  23873  prdsxmet  23875  fsumcn  24386  ovolfiniun  25018  ovoliunnul  25024  volfiniun  25064  iunmbl  25070  limciun  25411  dvfsumle  25538  dvfsumabs  25540  dvfsumlem1  25543  dvfsumlem3  25545  dvfsumlem4  25546  dvfsumrlim  25548  dvfsumrlim2  25549  dvfsum2  25551  itgsubst  25566  fsumvma  26716  dchrisumlema  26991  dchrisumlem2  26993  dchrisumlem3  26994  nosupbnd1  27217  noinfbnd1  27232  chirred  31648  fsumiunle  32035  sigapildsyslem  33159  voliune  33227  volfiniune  33228  gg-dvfsumle  35182  ptrest  36487  poimirlem25  36513  poimirlem26  36514  mzpsubst  41486  rabdiophlem2  41540  cvgcaule  44202  etransclem48  44998  sge0iunmpt  45134  2reu8i  45821