Theorem rspc 3552

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540   = wceq 1542  Ⅎwnf 1785   ∈ wcel 2114  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-nf 1786  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052

This theorem is referenced by:  rspc2  3573  rspc2vd  3885  disjxiun  5082  pofun  5557  fmptcof  7083  fliftfuns  7269  ofmpteq  7654  tfisg  7805  qliftfuns  8751  xpf1o  9077  iunfi  9253  iundom2g  10462  lble  12108  rlimcld2  15540  sumeq2ii  15655  summolem3  15676  zsum  15680  fsum  15682  fsumf1o  15685  sumss2  15688  fsumcvg2  15689  fsumadd  15702  isummulc2  15724  fsum2dlem  15732  fsumcom2  15736  fsumshftm  15743  fsum0diag2  15745  fsummulc2  15746  fsum00  15761  fsumabs  15764  fsumrelem  15770  fsumrlim  15774  fsumo1  15775  o1fsum  15776  fsumiun  15784  isumshft  15804  prodeq2ii  15876  prodmolem3  15898  zprod  15902  fprod  15906  fprodf1o  15911  prodss  15912  fprodser  15914  fprodmul  15925  fproddiv  15926  fprodm1s  15935  fprodp1s  15936  fprodabs  15939  fprod2dlem  15945  fprodcom2  15949  fprodefsum  16060  sumeven  16356  sumodd  16357  pcmpt  16863  invfuc  17944  dprd2d2  20021  txcnp  23585  ptcnplem  23586  prdsdsf  24332  prdsxmet  24334  fsumcn  24837  ovolfiniun  25468  ovoliunnul  25474  volfiniun  25514  iunmbl  25520  limciun  25861  dvfsumle  25988  dvfsumabs  25990  dvfsumlem1  25993  dvfsumlem3  25995  dvfsumlem4  25996  dvfsumrlim  25998  dvfsumrlim2  25999  dvfsum2  26001  itgsubst  26016  fsumvma  27176  dchrisumlema  27451  dchrisumlem2  27453  dchrisumlem3  27454  nosupbnd1  27678  noinfbnd1  27693  chirred  32466  fsumiunle  32902  sigapildsyslem  34305  voliune  34373  volfiniune  34374  ptrest  37940  poimirlem25  37966  poimirlem26  37967  mzpsubst  43180  rabdiophlem2  43230  cvgcaule  45919  etransclem48  46710  sge0iunmpt  46846  2reu8i  47561