Theorem rspc 3565

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 3078	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
2		nfcv 2923	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfv 1947	. . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
4		rspc.1	. . . . 5 ⊢ Ⅎ𝑥𝜓
5	3, 4	nfim 1929	. . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓)
6		eleq1 2849	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
7		rspc.2	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
8	6, 7	imbi12d 347	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))
9	2, 5, 8	spcgf 3546	. . 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 3077

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 2213  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-nf 1817  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078

This theorem is used by:  rspc2  3585  rspc2vd  3895  disjxiun  5100  pofun  5577  fmptcof  7123  fliftfuns  7314  ofmpteq  7705  tfisg  7854  qliftfuns  8809  xpf1o  9142  iunfi  9316  iundom2g  10605  lble  12250  rlimcld2  15725  sumeq2ii  15840  summolem3  15860  zsum  15864  fsum  15866  fsumf1o  15869  sumss2  15872  fsumcvg2  15873  fsumadd  15886  isummulc2  15908  fsum2dlem  15916  fsumcom2  15920  fsumshftm  15927  fsum0diag2  15929  fsummulc2  15930  fsum00  15945  fsumabs  15948  fsumrelem  15954  fsumrlim  15958  fsumo1  15959  o1fsum  15960  fsumiun  15968  isumshft  15988  prodeq2ii  16060  prodmolem3  16080  zprod  16084  fprod  16088  fprodf1o  16093  prodss  16094  fprodser  16096  fprodmul  16107  fproddiv  16108  fprodm1s  16117  fprodp1s  16118  fprodabs  16121  fprod2dlem  16127  fprodcom2  16131  fprodefsum  16241  sumeven  16537  sumodd  16538  pcmpt  17050  invfuc  18132  dprd2d2  20240  txcnp  23919  ptcnplem  23920  prdsdsf  24666  prdsxmet  24668  fsumcn  25171  ovolfiniun  25802  ovoliunnul  25808  volfiniun  25848  iunmbl  25854  limciun  26194  dvfsumle  26321  dvfsumabs  26323  dvfsumlem1  26326  dvfsumlem3  26328  dvfsumlem4  26329  dvfsumrlim  26331  dvfsumrlim2  26332  dvfsum2  26334  itgsubst  26349  fsumvma  27522  dchrisumlema  27797  dchrisumlem2  27799  dchrisumlem3  27800  nosupbnd1  28053  noinfbnd1  28068  chirred  32979  fsumiunle  33402  sigapildsyslem  34776  voliune  34844  volfiniune  34845  ptrest  38505  poimirlem25  38531  poimirlem26  38532  mzpsubst  43712  rabdiophlem2  43762  cvgcaule  46445  etransclem48  47236  sge0iunmpt  47372  2reu8i  48127