Theorem rspc 3576

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 3045	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
2		nfcv 2891	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfv 1914	. . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
4		rspc.1	. . . . 5 ⊢ Ⅎ𝑥𝜓
5	3, 4	nfim 1896	. . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓)
6		eleq1 2816	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
7		rspc.2	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
8	6, 7	imbi12d 344	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))
9	2, 5, 8	spcgf 3557	. . 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 2109  ∀wral 3044

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-nf 1784  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045

This theorem is referenced by:  rspc2  3597  rspc2vd  3910  disjxiun  5104  pofun  5564  fmptcof  7102  fliftfuns  7289  ofmpteq  7676  tfisg  7830  qliftfuns  8777  xpf1o  9103  iunfi  9294  iundom2g  10493  lble  12135  rlimcld2  15544  sumeq2ii  15659  summolem3  15680  zsum  15684  fsum  15686  fsumf1o  15689  sumss2  15692  fsumcvg2  15693  fsumadd  15706  isummulc2  15728  fsum2dlem  15736  fsumcom2  15740  fsumshftm  15747  fsum0diag2  15749  fsummulc2  15750  fsum00  15764  fsumabs  15767  fsumrelem  15773  fsumrlim  15777  fsumo1  15778  o1fsum  15779  fsumiun  15787  isumshft  15805  prodeq2ii  15877  prodmolem3  15899  zprod  15903  fprod  15907  fprodf1o  15912  prodss  15913  fprodser  15915  fprodmul  15926  fproddiv  15927  fprodm1s  15936  fprodp1s  15937  fprodabs  15940  fprod2dlem  15946  fprodcom2  15950  fprodefsum  16061  sumeven  16357  sumodd  16358  pcmpt  16863  invfuc  17939  dprd2d2  19976  txcnp  23507  ptcnplem  23508  prdsdsf  24255  prdsxmet  24257  fsumcn  24761  ovolfiniun  25402  ovoliunnul  25408  volfiniun  25448  iunmbl  25454  limciun  25795  dvfsumle  25926  dvfsumleOLD  25927  dvfsumabs  25929  dvfsumlem1  25932  dvfsumlem3  25935  dvfsumlem4  25936  dvfsumrlim  25938  dvfsumrlim2  25939  dvfsum2  25941  itgsubst  25956  fsumvma  27124  dchrisumlema  27399  dchrisumlem2  27401  dchrisumlem3  27402  nosupbnd1  27626  noinfbnd1  27641  chirred  32324  fsumiunle  32754  sigapildsyslem  34151  voliune  34219  volfiniune  34220  ptrest  37613  poimirlem25  37639  poimirlem26  37640  mzpsubst  42736  rabdiophlem2  42790  cvgcaule  45487  etransclem48  46280  sge0iunmpt  46416  2reu8i  47114