Theorem rspc 3569

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 3076	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
2		nfcv 2923	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfv 1933	. . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
4		rspc.1	. . . . 5 ⊢ Ⅎ𝑥𝜓
5	3, 4	nfim 1915	. . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓)
6		eleq1 2849	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
7		rspc.2	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
8	6, 7	imbi12d 346	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))
9	2, 5, 8	spcgf 3550	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → (𝐴 ∈ 𝐵 → 𝜓)))
10	9	pm2.43a 54	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → 𝜓))
11	1, 10	biimtrid 244	1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1557   = wceq 1559  Ⅎwnf 1802   ∈ wcel 2141  ∀wral 3075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-ex 1799  df-nf 1803  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3076

This theorem is referenced by:  rspc2  3590  rspc2vd  3900  disjxiun  5096  pofun  5571  fmptcof  7108  fliftfuns  7294  ofmpteq  7679  tfisg  7830  qliftfuns  8781  xpf1o  9107  iunfi  9283  iundom2g  10494  lble  12141  rlimcld2  15588  sumeq2ii  15703  summolem3  15724  zsum  15728  fsum  15730  fsumf1o  15733  sumss2  15736  fsumcvg2  15737  fsumadd  15750  isummulc2  15772  fsum2dlem  15780  fsumcom2  15784  fsumshftm  15791  fsum0diag2  15793  fsummulc2  15794  fsum00  15809  fsumabs  15812  fsumrelem  15818  fsumrlim  15822  fsumo1  15823  o1fsum  15824  fsumiun  15832  isumshft  15852  prodeq2ii  15924  prodmolem3  15946  zprod  15950  fprod  15954  fprodf1o  15959  prodss  15960  fprodser  15962  fprodmul  15973  fproddiv  15974  fprodm1s  15983  fprodp1s  15984  fprodabs  15987  fprod2dlem  15993  fprodcom2  15997  fprodefsum  16108  sumeven  16404  sumodd  16405  pcmpt  16911  invfuc  17993  dprd2d2  20069  txcnp  23660  ptcnplem  23661  prdsdsf  24407  prdsxmet  24409  fsumcn  24912  ovolfiniun  25543  ovoliunnul  25549  volfiniun  25589  iunmbl  25595  limciun  25936  dvfsumle  26063  dvfsumabs  26065  dvfsumlem1  26068  dvfsumlem3  26070  dvfsumlem4  26071  dvfsumrlim  26073  dvfsumrlim2  26074  dvfsum2  26076  itgsubst  26091  fsumvma  27254  dchrisumlema  27529  dchrisumlem2  27531  dchrisumlem3  27532  nosupbnd1  27755  noinfbnd1  27770  chirred  32544  fsumiunle  32981  sigapildsyslem  34419  voliune  34487  volfiniune  34488  ptrest  38082  poimirlem25  38108  poimirlem26  38109  mzpsubst  43293  rabdiophlem2  43343  cvgcaule  46029  etransclem48  46820  sge0iunmpt  46956  2reu8i  47671