Theorem rspc 2787

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 2422	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
2		nfcv 2282	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfv 1509	. . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
4		rspc.1	. . . . 5 ⊢ Ⅎ𝑥𝜓
5	3, 4	nfim 1552	. . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓)
6		eleq1 2203	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
7		rspc.2	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
8	6, 7	imbi12d 233	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))
9	2, 5, 8	spcgf 2771	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → (𝐴 ∈ 𝐵 → 𝜓)))
10	9	pm2.43a 51	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → 𝜓))
11	1, 10	syl5bi 151	1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 104  ∀wal 1330   = wceq 1332  Ⅎwnf 1437   ∈ wcel 1481  ∀wral 2417

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-v 2691

This theorem is referenced by:  rspcv  2789  rspc2  2804  pofun  4242  omsinds  4543  fmptcof  5595  fliftfuns  5707  qliftfuns  6521  xpf1o  6746  finexdc  6804  ssfirab  6830  iunfidisj  6842  cc3  7100  lble  8729  exfzdc  10048  uzsinds  10246  sumeq2  11160  sumfct  11175  sumrbdclem  11178  summodclem3  11181  summodclem2a  11182  zsumdc  11185  fsumgcl  11187  fsum3  11188  fsumf1o  11191  isumss  11192  isumss2  11194  fsum3cvg2  11195  fsumadd  11207  isummulc2  11227  fsum2dlemstep  11235  fisumcom2  11239  fsumshftm  11246  fisum0diag2  11248  fsummulc2  11249  fsum00  11263  fsumabs  11266  fsumrelem  11272  fsumiun  11278  isumshft  11291  mertenslem2  11337  prodeq2  11358  prodrbdclem  11372  prodmodclem3  11376  prodmodclem2a  11377  zproddc  11380  fprodseq  11384  zsupcllemstep  11674  infssuzex  11678  bezoutlemmain  11722  ctiunctlemudc  11986  iuncld  12323  txcnp  12479  fsumcncntop  12764  bj-nntrans  13320