Theorem rspc 2837

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

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1351   = wceq 1353  Ⅎwnf 1460   ∈ wcel 2148  ∀wral 2455

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-v 2741

This theorem is referenced by:  rspcv  2839  rspc2  2854  rspc2vd  3127  pofun  4314  omsinds  4623  fmptcof  5686  fliftfuns  5802  qliftfuns  6622  xpf1o  6847  finexdc  6905  ssfirab  6936  iunfidisj  6948  dcfi  6983  cc3  7270  lble  8907  exfzdc  10243  uzsinds  10445  sumeq2  11370  sumfct  11385  sumrbdclem  11388  summodclem3  11391  summodclem2a  11392  zsumdc  11395  fsumgcl  11397  fsum3  11398  fsumf1o  11401  isumss  11402  isumss2  11404  fsum3cvg2  11405  fsumadd  11417  isummulc2  11437  fsum2dlemstep  11445  fisumcom2  11449  fsumshftm  11456  fisum0diag2  11458  fsummulc2  11459  fsum00  11473  fsumabs  11476  fsumrelem  11482  fsumiun  11488  isumshft  11501  mertenslem2  11547  prodeq2  11568  prodrbdclem  11582  prodmodclem3  11586  prodmodclem2a  11587  zproddc  11590  fprodseq  11594  prodfct  11598  fprodf1o  11599  prodssdc  11600  fprodmul  11602  fprodm1s  11612  fprodp1s  11613  fprodabs  11627  fprodap0  11632  fprod2dlemstep  11633  fprodcom2fi  11637  fprodrec  11640  fprodap0f  11647  fprodle  11651  zsupcllemstep  11949  infssuzex  11953  bezoutlemmain  12002  nnwosdc  12043  pcmpt  12344  ctiunctlemudc  12441  iuncld  13755  txcnp  13911  fsumcncntop  14196  bj-nntrans  14843