Theorem rspc 3567

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 3045	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
2		nfcv 2891	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfv 1914	. . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
4		rspc.1	. . . . 5 ⊢ Ⅎ𝑥𝜓
5	3, 4	nfim 1896	. . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓)
6		eleq1 2816	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
7		rspc.2	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
8	6, 7	imbi12d 344	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))
9	2, 5, 8	spcgf 3548	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → (𝐴 ∈ 𝐵 → 𝜓)))
10	9	pm2.43a 54	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → 𝜓))
11	1, 10	biimtrid 242	1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538   = wceq 1540  Ⅎwnf 1783   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-nf 1784  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045

This theorem is referenced by:  rspc2  3588  rspc2vd  3901  disjxiun  5092  pofun  5549  fmptcof  7068  fliftfuns  7255  ofmpteq  7640  tfisg  7794  qliftfuns  8738  xpf1o  9063  iunfi  9252  iundom2g  10453  lble  12095  rlimcld2  15503  sumeq2ii  15618  summolem3  15639  zsum  15643  fsum  15645  fsumf1o  15648  sumss2  15651  fsumcvg2  15652  fsumadd  15665  isummulc2  15687  fsum2dlem  15695  fsumcom2  15699  fsumshftm  15706  fsum0diag2  15708  fsummulc2  15709  fsum00  15723  fsumabs  15726  fsumrelem  15732  fsumrlim  15736  fsumo1  15737  o1fsum  15738  fsumiun  15746  isumshft  15764  prodeq2ii  15836  prodmolem3  15858  zprod  15862  fprod  15866  fprodf1o  15871  prodss  15872  fprodser  15874  fprodmul  15885  fproddiv  15886  fprodm1s  15895  fprodp1s  15896  fprodabs  15899  fprod2dlem  15905  fprodcom2  15909  fprodefsum  16020  sumeven  16316  sumodd  16317  pcmpt  16822  invfuc  17902  dprd2d2  19943  txcnp  23523  ptcnplem  23524  prdsdsf  24271  prdsxmet  24273  fsumcn  24777  ovolfiniun  25418  ovoliunnul  25424  volfiniun  25464  iunmbl  25470  limciun  25811  dvfsumle  25942  dvfsumleOLD  25943  dvfsumabs  25945  dvfsumlem1  25948  dvfsumlem3  25951  dvfsumlem4  25952  dvfsumrlim  25954  dvfsumrlim2  25955  dvfsum2  25957  itgsubst  25972  fsumvma  27140  dchrisumlema  27415  dchrisumlem2  27417  dchrisumlem3  27418  nosupbnd1  27642  noinfbnd1  27657  chirred  32357  fsumiunle  32787  sigapildsyslem  34127  voliune  34195  volfiniune  34196  ptrest  37598  poimirlem25  37624  poimirlem26  37625  mzpsubst  42721  rabdiophlem2  42775  cvgcaule  45471  etransclem48  46264  sge0iunmpt  46400  2reu8i  47098