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 3048	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
2		nfcv 2894	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfv 1915	. . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
4		rspc.1	. . . . 5 ⊢ Ⅎ𝑥𝜓
5	3, 4	nfim 1897	. . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓)
6		eleq1 2819	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
7		rspc.2	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
8	6, 7	imbi12d 344	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))
9	2, 5, 8	spcgf 3546	. . 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 2111  ∀wral 3047

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-nf 1785  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ral 3048

This theorem is referenced by:  rspc2  3586  rspc2vd  3898  disjxiun  5088  pofun  5542  fmptcof  7063  fliftfuns  7248  ofmpteq  7633  tfisg  7784  qliftfuns  8728  xpf1o  9052  iunfi  9227  iundom2g  10431  lble  12074  rlimcld2  15485  sumeq2ii  15600  summolem3  15621  zsum  15625  fsum  15627  fsumf1o  15630  sumss2  15633  fsumcvg2  15634  fsumadd  15647  isummulc2  15669  fsum2dlem  15677  fsumcom2  15681  fsumshftm  15688  fsum0diag2  15690  fsummulc2  15691  fsum00  15705  fsumabs  15708  fsumrelem  15714  fsumrlim  15718  fsumo1  15719  o1fsum  15720  fsumiun  15728  isumshft  15746  prodeq2ii  15818  prodmolem3  15840  zprod  15844  fprod  15848  fprodf1o  15853  prodss  15854  fprodser  15856  fprodmul  15867  fproddiv  15868  fprodm1s  15877  fprodp1s  15878  fprodabs  15881  fprod2dlem  15887  fprodcom2  15891  fprodefsum  16002  sumeven  16298  sumodd  16299  pcmpt  16804  invfuc  17884  dprd2d2  19959  txcnp  23536  ptcnplem  23537  prdsdsf  24283  prdsxmet  24285  fsumcn  24789  ovolfiniun  25430  ovoliunnul  25436  volfiniun  25476  iunmbl  25482  limciun  25823  dvfsumle  25954  dvfsumleOLD  25955  dvfsumabs  25957  dvfsumlem1  25960  dvfsumlem3  25963  dvfsumlem4  25964  dvfsumrlim  25966  dvfsumrlim2  25967  dvfsum2  25969  itgsubst  25984  fsumvma  27152  dchrisumlema  27427  dchrisumlem2  27429  dchrisumlem3  27430  nosupbnd1  27654  noinfbnd1  27669  chirred  32373  fsumiunle  32810  sigapildsyslem  34172  voliune  34240  volfiniune  34241  ptrest  37665  poimirlem25  37691  poimirlem26  37692  mzpsubst  42787  rabdiophlem2  42841  cvgcaule  45535  etransclem48  46326  sge0iunmpt  46462  2reu8i  47150