Theorem rspc 3570

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

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1568   = wceq 1570  Ⅎwnf 1813   ∈ wcel 2143  ∀wral 3079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1810  df-nf 1814  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080

This theorem is referenced by:  rspc2  3591  rspc2vd  3902  disjxiun  5107  pofun  5589  fmptcof  7128  fliftfuns  7314  ofmpteq  7699  tfisg  7851  qliftfuns  8803  xpf1o  9128  iunfi  9301  iundom2g  10525  lble  12168  rlimcld2  15631  sumeq2ii  15746  summolem3  15767  zsum  15771  fsum  15773  fsumf1o  15776  sumss2  15779  fsumcvg2  15780  fsumadd  15793  isummulc2  15815  fsum2dlem  15823  fsumcom2  15827  fsumshftm  15834  fsum0diag2  15836  fsummulc2  15837  fsum00  15852  fsumabs  15855  fsumrelem  15861  fsumrlim  15865  fsumo1  15866  o1fsum  15867  fsumiun  15875  isumshft  15895  prodeq2ii  15967  prodmolem3  15989  zprod  15993  fprod  15997  fprodf1o  16002  prodss  16003  fprodser  16005  fprodmul  16016  fproddiv  16017  fprodm1s  16026  fprodp1s  16027  fprodabs  16030  fprod2dlem  16036  fprodcom2  16040  fprodefsum  16150  sumeven  16446  sumodd  16447  pcmpt  16953  invfuc  18035  dprd2d2  20117  txcnp  23758  ptcnplem  23759  prdsdsf  24505  prdsxmet  24507  fsumcn  25010  ovolfiniun  25641  ovoliunnul  25647  volfiniun  25687  iunmbl  25693  limciun  26034  dvfsumle  26161  dvfsumabs  26163  dvfsumlem1  26166  dvfsumlem3  26168  dvfsumlem4  26169  dvfsumrlim  26171  dvfsumrlim2  26172  dvfsum2  26174  itgsubst  26189  fsumvma  27355  dchrisumlema  27630  dchrisumlem2  27632  dchrisumlem3  27633  nosupbnd1  27856  noinfbnd1  27871  chirred  32725  fsumiunle  33151  sigapildsyslem  34529  voliune  34597  volfiniune  34598  ptrest  38248  poimirlem25  38274  poimirlem26  38275  mzpsubst  43459  rabdiophlem2  43509  cvgcaule  46185  etransclem48  46976  sge0iunmpt  47112  2reu8i  47827