Theorem rspc 3555

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 3055	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
2		nfcv 2902	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfv 1921	. . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
4		rspc.1	. . . . 5 ⊢ Ⅎ𝑥𝜓
5	3, 4	nfim 1903	. . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓)
6		eleq1 2828	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
7		rspc.2	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
8	6, 7	imbi12d 345	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))
9	2, 5, 8	spcgf 3536	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → (𝐴 ∈ 𝐵 → 𝜓)))
10	9	pm2.43a 54	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → 𝜓))
11	1, 10	biimtrid 243	1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 207  ∀wal 1545   = wceq 1547  Ⅎwnf 1790   ∈ wcel 2119  ∀wral 3054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-ex 1787  df-nf 1791  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ral 3055

This theorem is referenced by:  rspc2  3576  rspc2vd  3886  disjxiun  5076  pofun  5551  fmptcof  7079  fliftfuns  7265  ofmpteq  7650  tfisg  7801  qliftfuns  8748  xpf1o  9074  iunfi  9250  iundom2g  10460  lble  12106  rlimcld2  15538  sumeq2ii  15653  summolem3  15674  zsum  15678  fsum  15680  fsumf1o  15683  sumss2  15686  fsumcvg2  15687  fsumadd  15700  isummulc2  15722  fsum2dlem  15730  fsumcom2  15734  fsumshftm  15741  fsum0diag2  15743  fsummulc2  15744  fsum00  15759  fsumabs  15762  fsumrelem  15768  fsumrlim  15772  fsumo1  15773  o1fsum  15774  fsumiun  15782  isumshft  15802  prodeq2ii  15874  prodmolem3  15896  zprod  15900  fprod  15904  fprodf1o  15909  prodss  15910  fprodser  15912  fprodmul  15923  fproddiv  15924  fprodm1s  15933  fprodp1s  15934  fprodabs  15937  fprod2dlem  15943  fprodcom2  15947  fprodefsum  16058  sumeven  16354  sumodd  16355  pcmpt  16861  invfuc  17942  dprd2d2  20019  txcnp  23610  ptcnplem  23611  prdsdsf  24357  prdsxmet  24359  fsumcn  24862  ovolfiniun  25493  ovoliunnul  25499  volfiniun  25539  iunmbl  25545  limciun  25886  dvfsumle  26013  dvfsumabs  26015  dvfsumlem1  26018  dvfsumlem3  26020  dvfsumlem4  26021  dvfsumrlim  26023  dvfsumrlim2  26024  dvfsum2  26026  itgsubst  26041  fsumvma  27201  dchrisumlema  27476  dchrisumlem2  27478  dchrisumlem3  27479  nosupbnd1  27703  noinfbnd1  27718  chirred  32491  fsumiunle  32928  sigapildsyslem  34352  voliune  34420  volfiniune  34421  ptrest  37993  poimirlem25  38019  poimirlem26  38020  mzpsubst  43204  rabdiophlem2  43254  cvgcaule  45941  etransclem48  46732  sge0iunmpt  46868  2reu8i  47583