Theorem rspc 3589

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 3052	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
2		nfcv 2898	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfv 1914	. . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
4		rspc.1	. . . . 5 ⊢ Ⅎ𝑥𝜓
5	3, 4	nfim 1896	. . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓)
6		eleq1 2822	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
7		rspc.2	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
8	6, 7	imbi12d 344	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))
9	2, 5, 8	spcgf 3570	. . 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 2108  ∀wral 3051

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-nf 1784  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052

This theorem is referenced by:  rspc2  3610  rspc2vd  3922  disjxiun  5116  pofun  5579  fmptcof  7119  fliftfuns  7306  ofmpteq  7692  tfisg  7847  qliftfuns  8816  xpf1o  9151  iunfi  9353  iundom2g  10552  lble  12192  rlimcld2  15592  sumeq2ii  15707  summolem3  15728  zsum  15732  fsum  15734  fsumf1o  15737  sumss2  15740  fsumcvg2  15741  fsumadd  15754  isummulc2  15776  fsum2dlem  15784  fsumcom2  15788  fsumshftm  15795  fsum0diag2  15797  fsummulc2  15798  fsum00  15812  fsumabs  15815  fsumrelem  15821  fsumrlim  15825  fsumo1  15826  o1fsum  15827  fsumiun  15835  isumshft  15853  prodeq2ii  15925  prodmolem3  15947  zprod  15951  fprod  15955  fprodf1o  15960  prodss  15961  fprodser  15963  fprodmul  15974  fproddiv  15975  fprodm1s  15984  fprodp1s  15985  fprodabs  15988  fprod2dlem  15994  fprodcom2  15998  fprodefsum  16109  sumeven  16404  sumodd  16405  pcmpt  16910  invfuc  17988  dprd2d2  20025  txcnp  23556  ptcnplem  23557  prdsdsf  24304  prdsxmet  24306  fsumcn  24810  ovolfiniun  25452  ovoliunnul  25458  volfiniun  25498  iunmbl  25504  limciun  25845  dvfsumle  25976  dvfsumleOLD  25977  dvfsumabs  25979  dvfsumlem1  25982  dvfsumlem3  25985  dvfsumlem4  25986  dvfsumrlim  25988  dvfsumrlim2  25989  dvfsum2  25991  itgsubst  26006  fsumvma  27174  dchrisumlema  27449  dchrisumlem2  27451  dchrisumlem3  27452  nosupbnd1  27676  noinfbnd1  27691  chirred  32322  fsumiunle  32754  sigapildsyslem  34138  voliune  34206  volfiniune  34207  ptrest  37589  poimirlem25  37615  poimirlem26  37616  mzpsubst  42718  rabdiophlem2  42772  cvgcaule  45466  etransclem48  46259  sge0iunmpt  46395  2reu8i  47090