Theorem rspc 3564

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 3077	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
2		nfcv 2922	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfv 1946	. . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
4		rspc.1	. . . . 5 ⊢ Ⅎ𝑥𝜓
5	3, 4	nfim 1928	. . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓)
6		eleq1 2848	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
7		rspc.2	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
8	6, 7	imbi12d 347	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))
9	2, 5, 8	spcgf 3545	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → (𝐴 ∈ 𝐵 → 𝜓)))
10	9	pm2.43a 55	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → 𝜓))
11	1, 10	biimtrid 245	1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1567   = wceq 1569  Ⅎwnf 1815   ∈ wcel 2144  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1812  df-nf 1816  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077

This theorem is used by:  rspc2  3584  rspc2vd  3894  disjxiun  5099  pofun  5576  fmptcof  7131  fliftfuns  7322  ofmpteq  7716  tfisg  7865  qliftfuns  8828  xpf1o  9161  iunfi  9335  iundom2g  10627  lble  12272  rlimcld2  15750  sumeq2ii  15865  summolem3  15885  zsum  15889  fsum  15891  fsumf1o  15894  sumss2  15897  fsumcvg2  15898  fsumadd  15911  isummulc2  15933  fsum2dlem  15941  fsumcom2  15945  fsumshftm  15952  fsum0diag2  15954  fsummulc2  15955  fsum00  15970  fsumabs  15973  fsumrelem  15979  fsumrlim  15983  fsumo1  15984  o1fsum  15985  fsumiun  15993  isumshft  16013  prodeq2ii  16085  prodmolem3  16105  zprod  16109  fprod  16113  fprodf1o  16118  prodss  16119  fprodser  16121  fprodmul  16132  fproddiv  16133  fprodm1s  16142  fprodp1s  16143  fprodabs  16146  fprod2dlem  16152  fprodcom2  16156  fprodefsum  16266  sumeven  16562  sumodd  16563  pcmpt  17075  invfuc  18157  dprd2d2  20265  txcnp  23944  ptcnplem  23945  prdsdsf  24691  prdsxmet  24693  fsumcn  25196  ovolfiniun  25827  ovoliunnul  25833  volfiniun  25873  iunmbl  25879  limciun  26219  dvfsumle  26346  dvfsumabs  26348  dvfsumlem1  26351  dvfsumlem3  26353  dvfsumlem4  26354  dvfsumrlim  26356  dvfsumrlim2  26357  dvfsum2  26359  itgsubst  26374  fsumvma  27545  dchrisumlema  27820  dchrisumlem2  27822  dchrisumlem3  27823  nosupbnd1  28076  noinfbnd1  28091  chirred  33002  fsumiunle  33466  sigapildsyslem  34840  voliune  34908  volfiniune  34909  ptrest  38630  poimirlem25  38656  poimirlem26  38657  mzpsubst  43852  rabdiophlem2  43902  cvgcaule  46594  etransclem48  47385  sge0iunmpt  47521  2reu8i  48276