Theorem rspc 3579

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 3046	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
2		nfcv 2892	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfv 1914	. . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
4		rspc.1	. . . . 5 ⊢ Ⅎ𝑥𝜓
5	3, 4	nfim 1896	. . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓)
6		eleq1 2817	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
7		rspc.2	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
8	6, 7	imbi12d 344	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))
9	2, 5, 8	spcgf 3560	. . 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 2109  ∀wral 3045

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-nf 1784  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046

This theorem is referenced by:  rspc2  3600  rspc2vd  3913  disjxiun  5107  pofun  5567  fmptcof  7105  fliftfuns  7292  ofmpteq  7679  tfisg  7833  qliftfuns  8780  xpf1o  9109  iunfi  9301  iundom2g  10500  lble  12142  rlimcld2  15551  sumeq2ii  15666  summolem3  15687  zsum  15691  fsum  15693  fsumf1o  15696  sumss2  15699  fsumcvg2  15700  fsumadd  15713  isummulc2  15735  fsum2dlem  15743  fsumcom2  15747  fsumshftm  15754  fsum0diag2  15756  fsummulc2  15757  fsum00  15771  fsumabs  15774  fsumrelem  15780  fsumrlim  15784  fsumo1  15785  o1fsum  15786  fsumiun  15794  isumshft  15812  prodeq2ii  15884  prodmolem3  15906  zprod  15910  fprod  15914  fprodf1o  15919  prodss  15920  fprodser  15922  fprodmul  15933  fproddiv  15934  fprodm1s  15943  fprodp1s  15944  fprodabs  15947  fprod2dlem  15953  fprodcom2  15957  fprodefsum  16068  sumeven  16364  sumodd  16365  pcmpt  16870  invfuc  17946  dprd2d2  19983  txcnp  23514  ptcnplem  23515  prdsdsf  24262  prdsxmet  24264  fsumcn  24768  ovolfiniun  25409  ovoliunnul  25415  volfiniun  25455  iunmbl  25461  limciun  25802  dvfsumle  25933  dvfsumleOLD  25934  dvfsumabs  25936  dvfsumlem1  25939  dvfsumlem3  25942  dvfsumlem4  25943  dvfsumrlim  25945  dvfsumrlim2  25946  dvfsum2  25948  itgsubst  25963  fsumvma  27131  dchrisumlema  27406  dchrisumlem2  27408  dchrisumlem3  27409  nosupbnd1  27633  noinfbnd1  27648  chirred  32331  fsumiunle  32761  sigapildsyslem  34158  voliune  34226  volfiniune  34227  ptrest  37620  poimirlem25  37646  poimirlem26  37647  mzpsubst  42743  rabdiophlem2  42797  cvgcaule  45494  etransclem48  46287  sge0iunmpt  46423  2reu8i  47118