Theorem rspc 3610

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538   = wceq 1540  Ⅎwnf 1783   ∈ wcel 2108  ∀wral 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780  df-nf 1784  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062

This theorem is referenced by:  rspc2  3631  rspc2vd  3947  disjxiun  5140  pofun  5610  fmptcof  7150  fliftfuns  7334  ofmpteq  7720  tfisg  7875  qliftfuns  8844  xpf1o  9179  iunfi  9383  iundom2g  10580  lble  12220  rlimcld2  15614  sumeq2ii  15729  summolem3  15750  zsum  15754  fsum  15756  fsumf1o  15759  sumss2  15762  fsumcvg2  15763  fsumadd  15776  isummulc2  15798  fsum2dlem  15806  fsumcom2  15810  fsumshftm  15817  fsum0diag2  15819  fsummulc2  15820  fsum00  15834  fsumabs  15837  fsumrelem  15843  fsumrlim  15847  fsumo1  15848  o1fsum  15849  fsumiun  15857  isumshft  15875  prodeq2ii  15947  prodmolem3  15969  zprod  15973  fprod  15977  fprodf1o  15982  prodss  15983  fprodser  15985  fprodmul  15996  fproddiv  15997  fprodm1s  16006  fprodp1s  16007  fprodabs  16010  fprod2dlem  16016  fprodcom2  16020  fprodefsum  16131  sumeven  16424  sumodd  16425  pcmpt  16930  invfuc  18022  dprd2d2  20064  txcnp  23628  ptcnplem  23629  prdsdsf  24377  prdsxmet  24379  fsumcn  24894  ovolfiniun  25536  ovoliunnul  25542  volfiniun  25582  iunmbl  25588  limciun  25929  dvfsumle  26060  dvfsumleOLD  26061  dvfsumabs  26063  dvfsumlem1  26066  dvfsumlem3  26069  dvfsumlem4  26070  dvfsumrlim  26072  dvfsumrlim2  26073  dvfsum2  26075  itgsubst  26090  fsumvma  27257  dchrisumlema  27532  dchrisumlem2  27534  dchrisumlem3  27535  nosupbnd1  27759  noinfbnd1  27774  chirred  32414  fsumiunle  32831  sigapildsyslem  34162  voliune  34230  volfiniune  34231  ptrest  37626  poimirlem25  37652  poimirlem26  37653  mzpsubst  42759  rabdiophlem2  42813  cvgcaule  45502  etransclem48  46297  sge0iunmpt  46433  2reu8i  47125