Theorem rspc 2902

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 2886	. . 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 2802

This theorem is referenced by:  rspcv  2904  rspc2  2919  rspc2vd  3194  pofun  4407  omsinds  4718  fmptcof  5810  fliftfuns  5934  qliftfuns  6783  xpf1o  7025  finexdc  7087  ssfirab  7123  opabfi  7126  iunfidisj  7139  dcfi  7174  cc3  7480  lble  9120  exfzdc  10479  zsupcllemstep  10482  infssuzex  10486  uzsinds  10699  sumeq2  11913  sumfct  11928  sumrbdclem  11931  summodclem3  11934  summodclem2a  11935  zsumdc  11938  fsumgcl  11940  fsum3  11941  fsumf1o  11944  isumss  11945  isumss2  11947  fsum3cvg2  11948  fsumadd  11960  isummulc2  11980  fsum2dlemstep  11988  fisumcom2  11992  fsumshftm  11999  fisum0diag2  12001  fsummulc2  12002  fsum00  12016  fsumabs  12019  fsumrelem  12025  fsumiun  12031  isumshft  12044  mertenslem2  12090  prodeq2  12111  prodrbdclem  12125  prodmodclem3  12129  prodmodclem2a  12130  zproddc  12133  fprodseq  12137  prodfct  12141  fprodf1o  12142  prodssdc  12143  fprodmul  12145  fprodm1s  12155  fprodp1s  12156  fprodabs  12170  fprodap0  12175  fprod2dlemstep  12176  fprodcom2fi  12180  fprodrec  12183  fprodap0f  12190  fprodle  12194  bezoutlemmain  12562  nnwosdc  12603  pcmpt  12909  ctiunctlemudc  13051  gsumfzfsumlemm  14594  iuncld  14832  txcnp  14988  fsumcncntop  15284  bj-nntrans  16496