Theorem rspc 2901

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

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1393   = wceq 1395  Ⅎwnf 1506   ∈ wcel 2200  ∀wral 2508

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-v 2801

This theorem is referenced by:  rspcv  2903  rspc2  2918  rspc2vd  3193  pofun  4400  omsinds  4711  fmptcof  5795  fliftfuns  5915  qliftfuns  6756  xpf1o  6993  finexdc  7052  ssfirab  7086  opabfi  7088  iunfidisj  7101  dcfi  7136  cc3  7442  lble  9082  exfzdc  10433  zsupcllemstep  10436  infssuzex  10440  uzsinds  10653  sumeq2  11856  sumfct  11871  sumrbdclem  11874  summodclem3  11877  summodclem2a  11878  zsumdc  11881  fsumgcl  11883  fsum3  11884  fsumf1o  11887  isumss  11888  isumss2  11890  fsum3cvg2  11891  fsumadd  11903  isummulc2  11923  fsum2dlemstep  11931  fisumcom2  11935  fsumshftm  11942  fisum0diag2  11944  fsummulc2  11945  fsum00  11959  fsumabs  11962  fsumrelem  11968  fsumiun  11974  isumshft  11987  mertenslem2  12033  prodeq2  12054  prodrbdclem  12068  prodmodclem3  12072  prodmodclem2a  12073  zproddc  12076  fprodseq  12080  prodfct  12084  fprodf1o  12085  prodssdc  12086  fprodmul  12088  fprodm1s  12098  fprodp1s  12099  fprodabs  12113  fprodap0  12118  fprod2dlemstep  12119  fprodcom2fi  12123  fprodrec  12126  fprodap0f  12133  fprodle  12137  bezoutlemmain  12505  nnwosdc  12546  pcmpt  12852  ctiunctlemudc  12994  gsumfzfsumlemm  14536  iuncld  14774  txcnp  14930  fsumcncntop  15226  bj-nntrans  16244