Theorem rspc 3599

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 3059	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
2		nfcv 2899	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfv 1909	. . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
4		rspc.1	. . . . 5 ⊢ Ⅎ𝑥𝜓
5	3, 4	nfim 1891	. . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓)
6		eleq1 2817	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
7		rspc.2	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
8	6, 7	imbi12d 343	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))
9	2, 5, 8	spcgf 3580	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → (𝐴 ∈ 𝐵 → 𝜓)))
10	9	pm2.43a 54	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → 𝜓))
11	1, 10	biimtrid 241	1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1531   = wceq 1533  Ⅎwnf 1777   ∈ wcel 2098  ∀wral 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ral 3059  df-v 3475

This theorem is referenced by:  rspc2  3620  rspc2vd  3945  disjxiun  5149  pofun  5612  fmptcof  7145  fliftfuns  7328  ofmpteq  7713  tfisg  7864  qliftfuns  8829  xpf1o  9170  iunfi  9372  iundom2g  10571  lble  12204  rlimcld2  15562  sumeq2ii  15679  summolem3  15700  zsum  15704  fsum  15706  fsumf1o  15709  sumss2  15712  fsumcvg2  15713  fsumadd  15726  isummulc2  15748  fsum2dlem  15756  fsumcom2  15760  fsumshftm  15767  fsum0diag2  15769  fsummulc2  15770  fsum00  15784  fsumabs  15787  fsumrelem  15793  fsumrlim  15797  fsumo1  15798  o1fsum  15799  fsumiun  15807  isumshft  15825  prodeq2ii  15897  prodmolem3  15917  zprod  15921  fprod  15925  fprodf1o  15930  prodss  15931  fprodser  15933  fprodmul  15944  fproddiv  15945  fprodm1s  15954  fprodp1s  15955  fprodabs  15958  fprod2dlem  15964  fprodcom2  15968  fprodefsum  16079  sumeven  16371  sumodd  16372  pcmpt  16868  invfuc  17973  dprd2d2  20008  txcnp  23544  ptcnplem  23545  prdsdsf  24293  prdsxmet  24295  fsumcn  24808  ovolfiniun  25450  ovoliunnul  25456  volfiniun  25496  iunmbl  25502  limciun  25843  dvfsumle  25974  dvfsumleOLD  25975  dvfsumabs  25977  dvfsumlem1  25980  dvfsumlem3  25983  dvfsumlem4  25984  dvfsumrlim  25986  dvfsumrlim2  25987  dvfsum2  25989  itgsubst  26004  fsumvma  27166  dchrisumlema  27441  dchrisumlem2  27443  dchrisumlem3  27444  nosupbnd1  27667  noinfbnd1  27682  chirred  32225  fsumiunle  32613  sigapildsyslem  33813  voliune  33881  volfiniune  33882  ptrest  37125  poimirlem25  37151  poimirlem26  37152  mzpsubst  42199  rabdiophlem2  42253  cvgcaule  44903  etransclem48  45699  sge0iunmpt  45835  2reu8i  46522