Theorem rspc 3561

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

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-nf 1785  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ral 3049

This theorem is referenced by:  rspc2  3582  rspc2vd  3894  disjxiun  5090  pofun  5545  fmptcof  7069  fliftfuns  7254  ofmpteq  7639  tfisg  7790  qliftfuns  8734  xpf1o  9059  iunfi  9234  iundom2g  10438  lble  12081  rlimcld2  15487  sumeq2ii  15602  summolem3  15623  zsum  15627  fsum  15629  fsumf1o  15632  sumss2  15635  fsumcvg2  15636  fsumadd  15649  isummulc2  15671  fsum2dlem  15679  fsumcom2  15683  fsumshftm  15690  fsum0diag2  15692  fsummulc2  15693  fsum00  15707  fsumabs  15710  fsumrelem  15716  fsumrlim  15720  fsumo1  15721  o1fsum  15722  fsumiun  15730  isumshft  15748  prodeq2ii  15820  prodmolem3  15842  zprod  15846  fprod  15850  fprodf1o  15855  prodss  15856  fprodser  15858  fprodmul  15869  fproddiv  15870  fprodm1s  15879  fprodp1s  15880  fprodabs  15883  fprod2dlem  15889  fprodcom2  15893  fprodefsum  16004  sumeven  16300  sumodd  16301  pcmpt  16806  invfuc  17886  dprd2d2  19960  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  32377  fsumiunle  32817  sigapildsyslem  34195  voliune  34263  volfiniune  34264  ptrest  37680  poimirlem25  37706  poimirlem26  37707  mzpsubst  42866  rabdiophlem2  42920  cvgcaule  45614  etransclem48  46405  sge0iunmpt  46541  2reu8i  47238