Theorem rspc 2828

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

Syntax hints:   → wi 4   ↔ wb 104  ∀wal 1346   = wceq 1348  Ⅎwnf 1453   ∈ wcel 2141  ∀wral 2448

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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-v 2732

This theorem is referenced by:  rspcv  2830  rspc2  2845  rspc2vd  3117  pofun  4297  omsinds  4606  fmptcof  5663  fliftfuns  5777  qliftfuns  6597  xpf1o  6822  finexdc  6880  ssfirab  6911  iunfidisj  6923  dcfi  6958  cc3  7230  lble  8863  exfzdc  10196  uzsinds  10398  sumeq2  11322  sumfct  11337  sumrbdclem  11340  summodclem3  11343  summodclem2a  11344  zsumdc  11347  fsumgcl  11349  fsum3  11350  fsumf1o  11353  isumss  11354  isumss2  11356  fsum3cvg2  11357  fsumadd  11369  isummulc2  11389  fsum2dlemstep  11397  fisumcom2  11401  fsumshftm  11408  fisum0diag2  11410  fsummulc2  11411  fsum00  11425  fsumabs  11428  fsumrelem  11434  fsumiun  11440  isumshft  11453  mertenslem2  11499  prodeq2  11520  prodrbdclem  11534  prodmodclem3  11538  prodmodclem2a  11539  zproddc  11542  fprodseq  11546  prodfct  11550  fprodf1o  11551  prodssdc  11552  fprodmul  11554  fprodm1s  11564  fprodp1s  11565  fprodabs  11579  fprodap0  11584  fprod2dlemstep  11585  fprodcom2fi  11589  fprodrec  11592  fprodap0f  11599  fprodle  11603  zsupcllemstep  11900  infssuzex  11904  bezoutlemmain  11953  nnwosdc  11994  pcmpt  12295  ctiunctlemudc  12392  iuncld  12909  txcnp  13065  fsumcncntop  13350  bj-nntrans  13986