Theorem rspc 2873

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

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1371   = wceq 1373  Ⅎwnf 1484   ∈ wcel 2177  ∀wral 2485

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-v 2775

This theorem is referenced by:  rspcv  2875  rspc2  2890  rspc2vd  3164  pofun  4364  omsinds  4675  fmptcof  5757  fliftfuns  5877  qliftfuns  6716  xpf1o  6953  finexdc  7011  ssfirab  7045  opabfi  7047  iunfidisj  7060  dcfi  7095  cc3  7393  lble  9033  exfzdc  10382  zsupcllemstep  10385  infssuzex  10389  uzsinds  10602  sumeq2  11720  sumfct  11735  sumrbdclem  11738  summodclem3  11741  summodclem2a  11742  zsumdc  11745  fsumgcl  11747  fsum3  11748  fsumf1o  11751  isumss  11752  isumss2  11754  fsum3cvg2  11755  fsumadd  11767  isummulc2  11787  fsum2dlemstep  11795  fisumcom2  11799  fsumshftm  11806  fisum0diag2  11808  fsummulc2  11809  fsum00  11823  fsumabs  11826  fsumrelem  11832  fsumiun  11838  isumshft  11851  mertenslem2  11897  prodeq2  11918  prodrbdclem  11932  prodmodclem3  11936  prodmodclem2a  11937  zproddc  11940  fprodseq  11944  prodfct  11948  fprodf1o  11949  prodssdc  11950  fprodmul  11952  fprodm1s  11962  fprodp1s  11963  fprodabs  11977  fprodap0  11982  fprod2dlemstep  11983  fprodcom2fi  11987  fprodrec  11990  fprodap0f  11997  fprodle  12001  bezoutlemmain  12369  nnwosdc  12410  pcmpt  12716  ctiunctlemudc  12858  gsumfzfsumlemm  14399  iuncld  14637  txcnp  14793  fsumcncntop  15089  bj-nntrans  16001