Theorem rspc 2917

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 2527	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
2		nfcv 2386	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfv 1577	. . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
4		rspc.1	. . . . 5 ⊢ Ⅎ𝑥𝜓
5	3, 4	nfim 1621	. . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓)
6		eleq1 2297	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
7		rspc.2	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
8	6, 7	imbi12d 234	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))
9	2, 5, 8	spcgf 2901	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → (𝐴 ∈ 𝐵 → 𝜓)))
10	9	pm2.43a 51	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → 𝜓))
11	1, 10	biimtrid 152	1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1396   = wceq 1398  Ⅎwnf 1509   ∈ wcel 2205  ∀wral 2522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-v 2817

This theorem is referenced by:  rspcv  2919  rspc2  2935  rspc2vd  3210  pofun  4438  omsinds  4749  fmptcof  5849  fliftfuns  5977  qliftfuns  6866  xpf1o  7110  finexdc  7173  ssfirab  7210  opabfi  7213  iunfidisj  7226  dcfi  7281  cc3  7598  lble  9238  exfzdc  10608  zsupcllemstep  10611  infssuzex  10615  uzsinds  10830  sumeq2  12069  sumfct  12084  sumrbdclem  12088  summodclem3  12091  summodclem2a  12092  zsumdc  12095  fsumgcl  12097  fsum3  12098  fsumf1o  12101  isumss  12102  isumss2  12104  fsum3cvg2  12105  fsumadd  12117  isummulc2  12137  fsum2dlemstep  12145  fisumcom2  12149  fsumshftm  12156  fisum0diag2  12158  fsummulc2  12159  fsum00  12173  fsumabs  12176  fsumrelem  12182  fsumiun  12188  isumshft  12201  mertenslem2  12247  prodeq2  12268  prodrbdclem  12282  prodmodclem3  12286  prodmodclem2a  12287  zproddc  12290  fprodseq  12294  prodfct  12298  fprodf1o  12299  prodssdc  12300  fprodmul  12302  fprodm1s  12312  fprodp1s  12313  fprodabs  12327  fprodap0  12332  fprod2dlemstep  12333  fprodcom2fi  12337  fprodrec  12340  fprodap0f  12347  fprodle  12351  bezoutlemmain  12719  nnwosdc  12760  pcmpt  13066  ctiunctlemudc  13272  gsumfzfsumlemm  14847  iuncld  15092  txcnp  15248  fsumcncntop  15544  bj-nntrans  16833