Theorem rspc 3567

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 3079	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
2		nfcv 2924	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfv 1947	. . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
4		rspc.1	. . . . 5 ⊢ Ⅎ𝑥𝜓
5	3, 4	nfim 1929	. . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓)
6		eleq1 2850	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
7		rspc.2	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
8	6, 7	imbi12d 347	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))
9	2, 5, 8	spcgf 3548	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → (𝐴 ∈ 𝐵 → 𝜓)))
10	9	pm2.43a 55	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → 𝜓))
11	1, 10	biimtrid 245	1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568   = wceq 1570  Ⅎwnf 1816   ∈ wcel 2145  ∀wral 3078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-nf 1817  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3079

This theorem is used by:  rspc2  3588  rspc2vd  3898  disjxiun  5104  pofun  5585  fmptcof  7128  fliftfuns  7319  ofmpteq  7705  tfisg  7854  qliftfuns  8808  xpf1o  9141  iunfi  9314  iundom2g  10552  lble  12195  rlimcld2  15669  sumeq2ii  15784  summolem3  15804  zsum  15808  fsum  15810  fsumf1o  15813  sumss2  15816  fsumcvg2  15817  fsumadd  15830  isummulc2  15852  fsum2dlem  15860  fsumcom2  15864  fsumshftm  15871  fsum0diag2  15873  fsummulc2  15874  fsum00  15889  fsumabs  15892  fsumrelem  15898  fsumrlim  15902  fsumo1  15903  o1fsum  15904  fsumiun  15912  isumshft  15932  prodeq2ii  16004  prodmolem3  16026  zprod  16030  fprod  16034  fprodf1o  16039  prodss  16040  fprodser  16042  fprodmul  16053  fproddiv  16054  fprodm1s  16063  fprodp1s  16064  fprodabs  16067  fprod2dlem  16073  fprodcom2  16077  fprodefsum  16187  sumeven  16483  sumodd  16484  pcmpt  16990  invfuc  18072  dprd2d2  20179  txcnp  23852  ptcnplem  23853  prdsdsf  24599  prdsxmet  24601  fsumcn  25104  ovolfiniun  25735  ovoliunnul  25741  volfiniun  25781  iunmbl  25787  limciun  26128  dvfsumle  26255  dvfsumabs  26257  dvfsumlem1  26260  dvfsumlem3  26262  dvfsumlem4  26263  dvfsumrlim  26265  dvfsumrlim2  26266  dvfsum2  26268  itgsubst  26283  fsumvma  27457  dchrisumlema  27732  dchrisumlem2  27734  dchrisumlem3  27735  nosupbnd1  27958  noinfbnd1  27973  chirred  32884  fsumiunle  33307  sigapildsyslem  34680  voliune  34748  volfiniune  34749  ptrest  38376  poimirlem25  38402  poimirlem26  38403  mzpsubst  43601  rabdiophlem2  43651  cvgcaule  46327  etransclem48  47118  sge0iunmpt  47254  2reu8i  48009