Theorem rspccva 3590

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 26-Jul-2006.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)

Hypothesis

Ref	Expression
rspcv.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
rspccva	⊢ ((∀𝑥 ∈ 𝐵 𝜑 ∧ 𝐴 ∈ 𝐵) → 𝜓)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rspccva

Step	Hyp	Ref	Expression
1		rspcv.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
2	1	rspcv 3587	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))
3	2	impcom 407	1 ⊢ ((∀𝑥 ∈ 𝐵 𝜑 ∧ 𝐴 ∈ 𝐵) → 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3045

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-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046

This theorem is referenced by:  disjne  4421  n0snor2el  4800  seex  5600  preddowncl  6308  frpoins3g  6322  foelrn  7082  foelrnf  7083  caofid0l  7689  caofid0r  7690  caofid1  7691  caofid2  7692  onnseq  8316  odi  8546  omsmolem  8624  naddssim  8652  fvixp  8878  unblem1  9246  ordiso2  9475  unwdomg  9544  ac5num  9996  acni2  10006  fodomacn  10016  iundom2g  10500  fpwwe2lem3  10593  eltsk2g  10711  tskpwss  10712  tskpw  10713  tsken  10714  prlem934  10993  dedekindle  11345  ltord1  11711  leord1  11712  eqord1  11713  ltord2  11714  leord2  11715  eqord2  11716  supmul1  12159  seqcaopr2  14010  bccl  14294  hashbc  14425  limsupbnd2  15456  2clim  15545  climsup  15643  caurcvg2  15651  caucvgb  15653  isummulc2  15735  telfsumo2  15776  fsumparts  15779  incexclem  15809  isumshft  15812  climcndslem1  15822  climcndslem2  15823  supcvg  15829  geomulcvg  15849  mertenslem2  15858  mertens  15859  bpolycl  16025  bpolydif  16028  rpnnen2lem10  16198  dvdsprime  16664  fuciso  17947  lubub  18477  lubl  18478  mgmlrid  18601  grpinvalem  18607  grpinvex  18882  issubg2  19080  issubg4  19084  nmzbi  19103  gagrpid  19233  cntzi  19268  psgnunilem2  19432  sylow1lem3  19537  pgpfi  19542  slwispgp  19548  sylow2alem1  19554  dprdfcl  19952  ablfac2  20028  abveq0  20734  issrngd  20771  phllmhm  21548  ipcl  21549  ipeq0  21554  isphld  21570  ocvi  21585  pf1ind  22249  cayhamlem3  22781  elcls3  22977  neindisj2  23017  perfi  23049  cnima  23159  1stcfb  23339  1stcelcls  23355  llyi  23368  nllyi  23369  locfinnei  23417  1stckgenlem  23447  ptbasin  23471  txcls  23498  ptcnp  23516  ufli  23808  tgpt0  24013  tsmsxplem2  24048  nrmmetd  24469  tngngp  24549  tngngp3  24551  reperflem  24714  lebnumlem3  24869  htpyi  24880  htpycc  24886  phtpyi  24890  cfili  25175  cmetcvg  25192  caubl  25215  caublcls  25216  bcthlem2  25232  bcthlem3  25233  bcthlem4  25234  ovolicc2lem1  25425  ovolicc2lem5  25429  ovolicc2  25430  voliunlem3  25460  volsuplem  25463  uniioombllem2  25491  mbfima  25538  ismbfd  25547  ismbf3d  25562  mbfmullem  25633  itg2monolem1  25658  itg2i1fseqle  25662  itg2i1fseq  25663  itg2i1fseq2  25664  itg2addlem  25666  bddmulibl  25747  bddiblnc  25750  c1liplem1  25908  dvfsumle  25933  dvfsumleOLD  25934  dvfsumabs  25936  dvfsumrlimf  25938  dvfsumlem1  25939  dvfsumlem2  25940  dvfsumlem2OLD  25941  dvfsumlem3  25942  dvfsumlem4  25943  dvfsumrlimge0  25944  dvfsum2  25948  ftc1lem6  25955  ulmcau  26311  ulmdvlem1  26316  ulmdvlem3  26318  mtestbdd  26321  itgulm  26324  radcnvlem1  26329  abelthlem5  26352  abelthlem7  26355  areambl  26875  2lgslem1a  27309  dchrisumlem2  27408  dchrvmasumiflem1  27419  pntpbnd1  27504  ostthlem1  27545  madebday  27818  addscom  27880  precsexlem9  28124  peano5n0s  28219  zs12bday  28350  tglowdim1i  28435  brbtwn2  28839  ax5seglem1  28862  ax5seglem2  28863  ax5seglem9  28871  axcontlem4  28901  axcontlem12  28909  fusgreghash2wsp  30274  grpoidinvlem3  30442  grpoidinv  30444  grpoidinv2  30451  vcidOLD  30500  minvecolem5  30817  hcaucvg  31122  hlimconvi  31127  lnopeq0i  31943  cnlnadjlem5  32007  csmdsymi  32270  difelsiga  34130  eulerpartlemb  34366  ballotlemfc0  34491  ballotlemfcc  34492  ptpconn  35227  cvmsdisj  35264  cvmshmeo  35265  snmlflim  35326  elmrsubrn  35514  mvtinf  35549  sinccvg  35667  fnemeet1  36361  fnemeet2  36362  fnejoin1  36363  fnejoin2  36364  bj-seex  36917  poimirlem27  37648  poimirlem32  37653  mblfinlem1  37658  ovoliunnfl  37663  ex-ovoliunnfl  37664  voliunnfl  37665  volsupnfl  37666  mbfresfi  37667  itg2gt0cn  37676  ftc1cnnc  37693  ftc1anc  37702  upixp  37730  filbcmb  37741  sdclem1  37744  seqpo  37748  incsequz2  37750  mettrifi  37758  caushft  37762  sstotbnd2  37775  heibor1lem  37810  heiborlem3  37814  heiborlem10  37821  heibor  37822  rrndstprj2  37832  cmpidelt  37860  rngoid  37903  fsuppind  42585  limsuc2  43037  cvgdvgrat  44309  cncmpmax  45033  mccllem  45602  mccl  45603  climinf  45611  climsuse  45613  islptre  45624  limcperiod  45633  addlimc  45653  0ellimcdiv  45654  cncficcgt0  45893  dvbdfbdioolem2  45934  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  dvnprodlem3  45953  stoweidlem7  46012  stoweidlem15  46020  stoweidlem21  46026  stoweidlem31  46036  stoweidlem35  46040  stoweidlem36  46041  stoweidlem50  46055  stoweidlem57  46062  stoweidlem59  46064  wallispilem3  46072  dirkercncflem2  46109  dirkercncflem4  46111  fourierdlem32  46144  fourierdlem33  46145  fourierdlem39  46151  fourierdlem62  46173  fourierdlem71  46182  fourierdlem89  46200  fourierdlem91  46202  fourierdlem93  46204  fourierdlem101  46212  fourierdlem103  46214  fourierdlem104  46215  etransclem24  46263  etransclem32  46271  smflimlem6  46781  smfpimcc  46813  smfsuplem2  46817  gricushgr  47921