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  4404  omsinds  4715  fmptcof  5807  fliftfuns  5931  qliftfuns  6779  xpf1o  7018  finexdc  7078  ssfirab  7114  opabfi  7116  iunfidisj  7129  dcfi  7164  cc3  7470  lble  9110  exfzdc  10463  zsupcllemstep  10466  infssuzex  10470  uzsinds  10683  sumeq2  11891  sumfct  11906  sumrbdclem  11909  summodclem3  11912  summodclem2a  11913  zsumdc  11916  fsumgcl  11918  fsum3  11919  fsumf1o  11922  isumss  11923  isumss2  11925  fsum3cvg2  11926  fsumadd  11938  isummulc2  11958  fsum2dlemstep  11966  fisumcom2  11970  fsumshftm  11977  fisum0diag2  11979  fsummulc2  11980  fsum00  11994  fsumabs  11997  fsumrelem  12003  fsumiun  12009  isumshft  12022  mertenslem2  12068  prodeq2  12089  prodrbdclem  12103  prodmodclem3  12107  prodmodclem2a  12108  zproddc  12111  fprodseq  12115  prodfct  12119  fprodf1o  12120  prodssdc  12121  fprodmul  12123  fprodm1s  12133  fprodp1s  12134  fprodabs  12148  fprodap0  12153  fprod2dlemstep  12154  fprodcom2fi  12158  fprodrec  12161  fprodap0f  12168  fprodle  12172  bezoutlemmain  12540  nnwosdc  12581  pcmpt  12887  ctiunctlemudc  13029  gsumfzfsumlemm  14572  iuncld  14810  txcnp  14966  fsumcncntop  15262  bj-nntrans  16423