Theorem rspc 2862

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

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1362   = wceq 1364  Ⅎwnf 1474   ∈ wcel 2167  ∀wral 2475

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-v 2765

This theorem is referenced by:  rspcv  2864  rspc2  2879  rspc2vd  3153  pofun  4347  omsinds  4658  fmptcof  5729  fliftfuns  5845  qliftfuns  6678  xpf1o  6905  finexdc  6963  ssfirab  6997  opabfi  6999  iunfidisj  7012  dcfi  7047  cc3  7335  lble  8974  exfzdc  10316  zsupcllemstep  10319  infssuzex  10323  uzsinds  10536  sumeq2  11524  sumfct  11539  sumrbdclem  11542  summodclem3  11545  summodclem2a  11546  zsumdc  11549  fsumgcl  11551  fsum3  11552  fsumf1o  11555  isumss  11556  isumss2  11558  fsum3cvg2  11559  fsumadd  11571  isummulc2  11591  fsum2dlemstep  11599  fisumcom2  11603  fsumshftm  11610  fisum0diag2  11612  fsummulc2  11613  fsum00  11627  fsumabs  11630  fsumrelem  11636  fsumiun  11642  isumshft  11655  mertenslem2  11701  prodeq2  11722  prodrbdclem  11736  prodmodclem3  11740  prodmodclem2a  11741  zproddc  11744  fprodseq  11748  prodfct  11752  fprodf1o  11753  prodssdc  11754  fprodmul  11756  fprodm1s  11766  fprodp1s  11767  fprodabs  11781  fprodap0  11786  fprod2dlemstep  11787  fprodcom2fi  11791  fprodrec  11794  fprodap0f  11801  fprodle  11805  bezoutlemmain  12165  nnwosdc  12206  pcmpt  12512  ctiunctlemudc  12654  gsumfzfsumlemm  14143  iuncld  14351  txcnp  14507  fsumcncntop  14803  bj-nntrans  15597