Theorem rspc 3553

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540   = wceq 1542  Ⅎwnf 1785   ∈ wcel 2114  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-nf 1786  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053

This theorem is referenced by:  rspc2  3574  rspc2vd  3886  disjxiun  5083  pofun  5550  fmptcof  7077  fliftfuns  7262  ofmpteq  7647  tfisg  7798  qliftfuns  8744  xpf1o  9070  iunfi  9246  iundom2g  10453  lble  12099  rlimcld2  15531  sumeq2ii  15646  summolem3  15667  zsum  15671  fsum  15673  fsumf1o  15676  sumss2  15679  fsumcvg2  15680  fsumadd  15693  isummulc2  15715  fsum2dlem  15723  fsumcom2  15727  fsumshftm  15734  fsum0diag2  15736  fsummulc2  15737  fsum00  15752  fsumabs  15755  fsumrelem  15761  fsumrlim  15765  fsumo1  15766  o1fsum  15767  fsumiun  15775  isumshft  15795  prodeq2ii  15867  prodmolem3  15889  zprod  15893  fprod  15897  fprodf1o  15902  prodss  15903  fprodser  15905  fprodmul  15916  fproddiv  15917  fprodm1s  15926  fprodp1s  15927  fprodabs  15930  fprod2dlem  15936  fprodcom2  15940  fprodefsum  16051  sumeven  16347  sumodd  16348  pcmpt  16854  invfuc  17935  dprd2d2  20012  txcnp  23595  ptcnplem  23596  prdsdsf  24342  prdsxmet  24344  fsumcn  24847  ovolfiniun  25478  ovoliunnul  25484  volfiniun  25524  iunmbl  25530  limciun  25871  dvfsumle  25998  dvfsumabs  26000  dvfsumlem1  26003  dvfsumlem3  26005  dvfsumlem4  26006  dvfsumrlim  26008  dvfsumrlim2  26009  dvfsum2  26011  itgsubst  26026  fsumvma  27190  dchrisumlema  27465  dchrisumlem2  27467  dchrisumlem3  27468  nosupbnd1  27692  noinfbnd1  27707  chirred  32481  fsumiunle  32917  sigapildsyslem  34321  voliune  34389  volfiniune  34390  ptrest  37954  poimirlem25  37980  poimirlem26  37981  mzpsubst  43194  rabdiophlem2  43248  cvgcaule  45937  etransclem48  46728  sge0iunmpt  46864  2reu8i  47573