Theorem rspc 2914

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 2525	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
2		nfcv 2384	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfv 1577	. . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
4		rspc.1	. . . . 5 ⊢ Ⅎ𝑥𝜓
5	3, 4	nfim 1621	. . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓)
6		eleq1 2295	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
7		rspc.2	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
8	6, 7	imbi12d 234	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))
9	2, 5, 8	spcgf 2898	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → (𝐴 ∈ 𝐵 → 𝜓)))
10	9	pm2.43a 51	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → 𝜓))
11	1, 10	biimtrid 152	1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1396   = wceq 1398  Ⅎwnf 1509   ∈ wcel 2203  ∀wral 2520

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-v 2814

This theorem is referenced by:  rspcv  2916  rspc2  2931  rspc2vd  3206  pofun  4432  omsinds  4743  fmptcof  5843  fliftfuns  5970  qliftfuns  6852  xpf1o  7096  finexdc  7159  ssfirab  7196  opabfi  7199  iunfidisj  7212  dcfi  7267  cc3  7581  lble  9220  exfzdc  10585  zsupcllemstep  10588  infssuzex  10592  uzsinds  10805  sumeq2  12040  sumfct  12055  sumrbdclem  12059  summodclem3  12062  summodclem2a  12063  zsumdc  12066  fsumgcl  12068  fsum3  12069  fsumf1o  12072  isumss  12073  isumss2  12075  fsum3cvg2  12076  fsumadd  12088  isummulc2  12108  fsum2dlemstep  12116  fisumcom2  12120  fsumshftm  12127  fisum0diag2  12129  fsummulc2  12130  fsum00  12144  fsumabs  12147  fsumrelem  12153  fsumiun  12159  isumshft  12172  mertenslem2  12218  prodeq2  12239  prodrbdclem  12253  prodmodclem3  12257  prodmodclem2a  12258  zproddc  12261  fprodseq  12265  prodfct  12269  fprodf1o  12270  prodssdc  12271  fprodmul  12273  fprodm1s  12283  fprodp1s  12284  fprodabs  12298  fprodap0  12303  fprod2dlemstep  12304  fprodcom2fi  12308  fprodrec  12311  fprodap0f  12318  fprodle  12322  bezoutlemmain  12690  nnwosdc  12731  pcmpt  13037  ctiunctlemudc  13180  gsumfzfsumlemm  14727  iuncld  14972  txcnp  15128  fsumcncntop  15424  bj-nntrans  16713