Theorem rspc 3572

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568   = wceq 1570  Ⅎwnf 1816   ∈ wcel 2146  ∀wral 3082

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-nf 1817  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ral 3083

This theorem is used by:  rspc2  3593  rspc2vd  3904  disjxiun  5111  pofun  5592  fmptcof  7133  fliftfuns  7323  ofmpteq  7710  tfisg  7859  qliftfuns  8811  xpf1o  9137  iunfi  9310  iundom2g  10542  lble  12185  rlimcld2  15655  sumeq2ii  15770  summolem3  15791  zsum  15795  fsum  15797  fsumf1o  15800  sumss2  15803  fsumcvg2  15804  fsumadd  15817  isummulc2  15839  fsum2dlem  15847  fsumcom2  15851  fsumshftm  15858  fsum0diag2  15860  fsummulc2  15861  fsum00  15876  fsumabs  15879  fsumrelem  15885  fsumrlim  15889  fsumo1  15890  o1fsum  15891  fsumiun  15899  isumshft  15919  prodeq2ii  15991  prodmolem3  16013  zprod  16017  fprod  16021  fprodf1o  16026  prodss  16027  fprodser  16029  fprodmul  16040  fproddiv  16041  fprodm1s  16050  fprodp1s  16051  fprodabs  16054  fprod2dlem  16060  fprodcom2  16064  fprodefsum  16174  sumeven  16470  sumodd  16471  pcmpt  16977  invfuc  18059  dprd2d2  20147  txcnp  23814  ptcnplem  23815  prdsdsf  24561  prdsxmet  24563  fsumcn  25066  ovolfiniun  25697  ovoliunnul  25703  volfiniun  25743  iunmbl  25749  limciun  26090  dvfsumle  26217  dvfsumabs  26219  dvfsumlem1  26222  dvfsumlem3  26224  dvfsumlem4  26225  dvfsumrlim  26227  dvfsumrlim2  26228  dvfsum2  26230  itgsubst  26245  fsumvma  27414  dchrisumlema  27689  dchrisumlem2  27691  dchrisumlem3  27692  nosupbnd1  27915  noinfbnd1  27930  chirred  32784  fsumiunle  33210  sigapildsyslem  34582  voliune  34650  volfiniune  34651  ptrest  38310  poimirlem25  38336  poimirlem26  38337  mzpsubst  43519  rabdiophlem2  43569  cvgcaule  46245  etransclem48  47036  sge0iunmpt  47172  2reu8i  47890