Theorem rspc 3623

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1535   = wceq 1537  Ⅎwnf 1781   ∈ wcel 2108  ∀wral 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-ex 1778  df-nf 1782  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068

This theorem is referenced by:  rspc2  3644  rspc2vd  3972  disjxiun  5163  pofun  5626  fmptcof  7164  fliftfuns  7350  ofmpteq  7736  tfisg  7891  qliftfuns  8862  xpf1o  9205  iunfi  9411  iundom2g  10609  lble  12247  rlimcld2  15624  sumeq2ii  15741  summolem3  15762  zsum  15766  fsum  15768  fsumf1o  15771  sumss2  15774  fsumcvg2  15775  fsumadd  15788  isummulc2  15810  fsum2dlem  15818  fsumcom2  15822  fsumshftm  15829  fsum0diag2  15831  fsummulc2  15832  fsum00  15846  fsumabs  15849  fsumrelem  15855  fsumrlim  15859  fsumo1  15860  o1fsum  15861  fsumiun  15869  isumshft  15887  prodeq2ii  15959  prodmolem3  15981  zprod  15985  fprod  15989  fprodf1o  15994  prodss  15995  fprodser  15997  fprodmul  16008  fproddiv  16009  fprodm1s  16018  fprodp1s  16019  fprodabs  16022  fprod2dlem  16028  fprodcom2  16032  fprodefsum  16143  sumeven  16435  sumodd  16436  pcmpt  16939  invfuc  18044  dprd2d2  20088  txcnp  23649  ptcnplem  23650  prdsdsf  24398  prdsxmet  24400  fsumcn  24913  ovolfiniun  25555  ovoliunnul  25561  volfiniun  25601  iunmbl  25607  limciun  25949  dvfsumle  26080  dvfsumleOLD  26081  dvfsumabs  26083  dvfsumlem1  26086  dvfsumlem3  26089  dvfsumlem4  26090  dvfsumrlim  26092  dvfsumrlim2  26093  dvfsum2  26095  itgsubst  26110  fsumvma  27275  dchrisumlema  27550  dchrisumlem2  27552  dchrisumlem3  27553  nosupbnd1  27777  noinfbnd1  27792  chirred  32427  fsumiunle  32833  sigapildsyslem  34125  voliune  34193  volfiniune  34194  ptrest  37579  poimirlem25  37605  poimirlem26  37606  mzpsubst  42704  rabdiophlem2  42758  cvgcaule  45407  etransclem48  46203  sge0iunmpt  46339  2reu8i  47028