Theorem rspc 3572

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 3080	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
2		nfcv 2927	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfv 1937	. . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
4		rspc.1	. . . . 5 ⊢ Ⅎ𝑥𝜓
5	3, 4	nfim 1919	. . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓)
6		eleq1 2853	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
7		rspc.2	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
8	6, 7	imbi12d 347	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))
9	2, 5, 8	spcgf 3553	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → (𝐴 ∈ 𝐵 → 𝜓)))
10	9	pm2.43a 55	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → 𝜓))
11	1, 10	biimtrid 245	1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1561   = wceq 1563  Ⅎwnf 1806   ∈ wcel 2145  ∀wral 3079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1803  df-nf 1807  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3080

This theorem is referenced by:  rspc2  3593  rspc2vd  3903  disjxiun  5102  pofun  5578  fmptcof  7116  fliftfuns  7302  ofmpteq  7687  tfisg  7838  qliftfuns  8790  xpf1o  9115  iunfi  9288  iundom2g  10512  lble  12158  rlimcld2  15619  sumeq2ii  15734  summolem3  15755  zsum  15759  fsum  15761  fsumf1o  15764  sumss2  15767  fsumcvg2  15768  fsumadd  15781  isummulc2  15803  fsum2dlem  15811  fsumcom2  15815  fsumshftm  15822  fsum0diag2  15824  fsummulc2  15825  fsum00  15840  fsumabs  15843  fsumrelem  15849  fsumrlim  15853  fsumo1  15854  o1fsum  15855  fsumiun  15863  isumshft  15883  prodeq2ii  15955  prodmolem3  15977  zprod  15981  fprod  15985  fprodf1o  15990  prodss  15991  fprodser  15993  fprodmul  16004  fproddiv  16005  fprodm1s  16014  fprodp1s  16015  fprodabs  16018  fprod2dlem  16024  fprodcom2  16028  fprodefsum  16139  sumeven  16435  sumodd  16436  pcmpt  16942  invfuc  18024  dprd2d2  20107  txcnp  23738  ptcnplem  23739  prdsdsf  24485  prdsxmet  24487  fsumcn  24990  ovolfiniun  25621  ovoliunnul  25627  volfiniun  25667  iunmbl  25673  limciun  26014  dvfsumle  26141  dvfsumabs  26143  dvfsumlem1  26146  dvfsumlem3  26148  dvfsumlem4  26149  dvfsumrlim  26151  dvfsumrlim2  26152  dvfsum2  26154  itgsubst  26169  fsumvma  27335  dchrisumlema  27610  dchrisumlem2  27612  dchrisumlem3  27613  nosupbnd1  27836  noinfbnd1  27851  chirred  32656  fsumiunle  33086  sigapildsyslem  34468  voliune  34536  volfiniune  34537  ptrest  38130  poimirlem25  38156  poimirlem26  38157  mzpsubst  43341  rabdiophlem2  43391  cvgcaule  46063  etransclem48  46854  sge0iunmpt  46990  2reu8i  47705