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  4403  omsinds  4714  fmptcof  5804  fliftfuns  5928  qliftfuns  6774  xpf1o  7013  finexdc  7072  ssfirab  7106  opabfi  7108  iunfidisj  7121  dcfi  7156  cc3  7462  lble  9102  exfzdc  10454  zsupcllemstep  10457  infssuzex  10461  uzsinds  10674  sumeq2  11878  sumfct  11893  sumrbdclem  11896  summodclem3  11899  summodclem2a  11900  zsumdc  11903  fsumgcl  11905  fsum3  11906  fsumf1o  11909  isumss  11910  isumss2  11912  fsum3cvg2  11913  fsumadd  11925  isummulc2  11945  fsum2dlemstep  11953  fisumcom2  11957  fsumshftm  11964  fisum0diag2  11966  fsummulc2  11967  fsum00  11981  fsumabs  11984  fsumrelem  11990  fsumiun  11996  isumshft  12009  mertenslem2  12055  prodeq2  12076  prodrbdclem  12090  prodmodclem3  12094  prodmodclem2a  12095  zproddc  12098  fprodseq  12102  prodfct  12106  fprodf1o  12107  prodssdc  12108  fprodmul  12110  fprodm1s  12120  fprodp1s  12121  fprodabs  12135  fprodap0  12140  fprod2dlemstep  12141  fprodcom2fi  12145  fprodrec  12148  fprodap0f  12155  fprodle  12159  bezoutlemmain  12527  nnwosdc  12568  pcmpt  12874  ctiunctlemudc  13016  gsumfzfsumlemm  14559  iuncld  14797  txcnp  14953  fsumcncntop  15249  bj-nntrans  16338