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  9241  exfzdc  10611  zsupcllemstep  10614  infssuzex  10618  uzsinds  10833  sumeq2  12073  sumfct  12088  sumrbdclem  12092  summodclem3  12095  summodclem2a  12096  zsumdc  12099  fsumgcl  12101  fsum3  12102  fsumf1o  12105  isumss  12106  isumss2  12108  fsum3cvg2  12109  fsumadd  12121  isummulc2  12141  fsum2dlemstep  12149  fisumcom2  12153  fsumshftm  12160  fisum0diag2  12162  fsummulc2  12163  fsum00  12177  fsumabs  12180  fsumrelem  12186  fsumiun  12192  isumshft  12205  mertenslem2  12251  prodeq2  12272  prodrbdclem  12286  prodmodclem3  12290  prodmodclem2a  12291  zproddc  12294  fprodseq  12298  prodfct  12302  fprodf1o  12303  prodssdc  12304  fprodmul  12306  fprodm1s  12316  fprodp1s  12317  fprodabs  12331  fprodap0  12336  fprod2dlemstep  12337  fprodcom2fi  12341  fprodrec  12344  fprodap0f  12351  fprodle  12355  bezoutlemmain  12723  nnwosdc  12764  pcmpt  13070  ctiunctlemudc  13276  gsumfzfsumlemm  14865  iuncld  15110  txcnp  15266  fsumcncntop  15562  bj-nntrans  16861