Theorem rspc 3566

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 3547	. . 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  3587  rspc2vd  3899  disjxiun  5097  pofun  5558  fmptcof  7085  fliftfuns  7270  ofmpteq  7655  tfisg  7806  qliftfuns  8753  xpf1o  9079  iunfi  9255  iundom2g  10462  lble  12106  rlimcld2  15513  sumeq2ii  15628  summolem3  15649  zsum  15653  fsum  15655  fsumf1o  15658  sumss2  15661  fsumcvg2  15662  fsumadd  15675  isummulc2  15697  fsum2dlem  15705  fsumcom2  15709  fsumshftm  15716  fsum0diag2  15718  fsummulc2  15719  fsum00  15733  fsumabs  15736  fsumrelem  15742  fsumrlim  15746  fsumo1  15747  o1fsum  15748  fsumiun  15756  isumshft  15774  prodeq2ii  15846  prodmolem3  15868  zprod  15872  fprod  15876  fprodf1o  15881  prodss  15882  fprodser  15884  fprodmul  15895  fproddiv  15896  fprodm1s  15905  fprodp1s  15906  fprodabs  15909  fprod2dlem  15915  fprodcom2  15919  fprodefsum  16030  sumeven  16326  sumodd  16327  pcmpt  16832  invfuc  17913  dprd2d2  19987  txcnp  23576  ptcnplem  23577  prdsdsf  24323  prdsxmet  24325  fsumcn  24829  ovolfiniun  25470  ovoliunnul  25476  volfiniun  25516  iunmbl  25522  limciun  25863  dvfsumle  25994  dvfsumleOLD  25995  dvfsumabs  25997  dvfsumlem1  26000  dvfsumlem3  26003  dvfsumlem4  26004  dvfsumrlim  26006  dvfsumrlim2  26007  dvfsum2  26009  itgsubst  26024  fsumvma  27192  dchrisumlema  27467  dchrisumlem2  27469  dchrisumlem3  27470  nosupbnd1  27694  noinfbnd1  27709  chirred  32482  fsumiunle  32920  sigapildsyslem  34338  voliune  34406  volfiniune  34407  ptrest  37864  poimirlem25  37890  poimirlem26  37891  mzpsubst  43099  rabdiophlem2  43153  cvgcaule  45843  etransclem48  46634  sge0iunmpt  46770  2reu8i  47467