Theorem rspc 3564

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 3052	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
2		nfcv 2898	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfv 1915	. . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
4		rspc.1	. . . . 5 ⊢ Ⅎ𝑥𝜓
5	3, 4	nfim 1897	. . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓)
6		eleq1 2824	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
7		rspc.2	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
8	6, 7	imbi12d 344	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))
9	2, 5, 8	spcgf 3545	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → (𝐴 ∈ 𝐵 → 𝜓)))
10	9	pm2.43a 54	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → 𝜓))
11	1, 10	biimtrid 242	1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539   = wceq 1541  Ⅎwnf 1784   ∈ wcel 2113  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-nf 1785  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052

This theorem is referenced by:  rspc2  3585  rspc2vd  3897  disjxiun  5095  pofun  5550  fmptcof  7075  fliftfuns  7260  ofmpteq  7645  tfisg  7796  qliftfuns  8741  xpf1o  9067  iunfi  9243  iundom2g  10450  lble  12094  rlimcld2  15501  sumeq2ii  15616  summolem3  15637  zsum  15641  fsum  15643  fsumf1o  15646  sumss2  15649  fsumcvg2  15650  fsumadd  15663  isummulc2  15685  fsum2dlem  15693  fsumcom2  15697  fsumshftm  15704  fsum0diag2  15706  fsummulc2  15707  fsum00  15721  fsumabs  15724  fsumrelem  15730  fsumrlim  15734  fsumo1  15735  o1fsum  15736  fsumiun  15744  isumshft  15762  prodeq2ii  15834  prodmolem3  15856  zprod  15860  fprod  15864  fprodf1o  15869  prodss  15870  fprodser  15872  fprodmul  15883  fproddiv  15884  fprodm1s  15893  fprodp1s  15894  fprodabs  15897  fprod2dlem  15903  fprodcom2  15907  fprodefsum  16018  sumeven  16314  sumodd  16315  pcmpt  16820  invfuc  17901  dprd2d2  19975  txcnp  23564  ptcnplem  23565  prdsdsf  24311  prdsxmet  24313  fsumcn  24817  ovolfiniun  25458  ovoliunnul  25464  volfiniun  25504  iunmbl  25510  limciun  25851  dvfsumle  25982  dvfsumleOLD  25983  dvfsumabs  25985  dvfsumlem1  25988  dvfsumlem3  25991  dvfsumlem4  25992  dvfsumrlim  25994  dvfsumrlim2  25995  dvfsum2  25997  itgsubst  26012  fsumvma  27180  dchrisumlema  27455  dchrisumlem2  27457  dchrisumlem3  27458  nosupbnd1  27682  noinfbnd1  27697  chirred  32470  fsumiunle  32910  sigapildsyslem  34318  voliune  34386  volfiniune  34387  ptrest  37816  poimirlem25  37842  poimirlem26  37843  mzpsubst  42986  rabdiophlem2  43040  cvgcaule  45731  etransclem48  46522  sge0iunmpt  46658  2reu8i  47355