Theorem rspccva 3611

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 3608	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))
3	2	impcom 407	1 ⊢ ((∀𝑥 ∈ 𝐵 𝜑 ∧ 𝐴 ∈ 𝐵) → 𝜓)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1540   ∈ wcel 2105  ∀wral 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061

This theorem is referenced by:  disjne  4454  n0snor2el  4834  seex  5638  preddowncl  6333  frpoins3g  6347  foelrn  7108  foelrnf  7109  caofid0l  7705  caofid0r  7706  caofid1  7707  caofid2  7708  onnseq  8350  odi  8585  omsmolem  8662  naddssim  8690  fvixp  8902  unblem1  9301  ordiso2  9516  unwdomg  9585  ac5num  10037  acni2  10047  fodomacn  10057  iundom2g  10541  fpwwe2lem3  10634  eltsk2g  10752  tskpwss  10753  tskpw  10754  tsken  10755  prlem934  11034  dedekindle  11385  ltord1  11747  leord1  11748  eqord1  11749  ltord2  11750  leord2  11751  eqord2  11752  supmul1  12190  seqcaopr2  14011  bccl  14289  hashbc  14419  limsupbnd2  15434  2clim  15523  climsup  15623  caurcvg2  15631  caucvgb  15633  isummulc2  15715  telfsumo2  15756  fsumparts  15759  incexclem  15789  isumshft  15792  climcndslem1  15802  climcndslem2  15803  supcvg  15809  geomulcvg  15829  mertenslem2  15838  mertens  15839  bpolycl  16003  bpolydif  16006  rpnnen2lem10  16173  dvdsprime  16631  fuciso  17938  lubub  18474  lubl  18475  mgmlrid  18598  grprinvlem  18604  grpinvex  18871  issubg2  19064  issubg4  19068  nmzbi  19087  gagrpid  19206  cntzi  19241  psgnunilem2  19411  sylow1lem3  19516  pgpfi  19521  slwispgp  19527  sylow2alem1  19533  dprdfcl  19931  ablfac2  20007  abveq0  20665  issrngd  20700  phllmhm  21495  ipcl  21496  ipeq0  21501  isphld  21517  ocvi  21532  psrbagconf1oOLD  21800  pf1ind  22194  cayhamlem3  22709  elcls3  22907  neindisj2  22947  perfi  22979  cnima  23089  1stcfb  23269  1stcelcls  23285  llyi  23298  nllyi  23299  locfinnei  23347  1stckgenlem  23377  ptbasin  23401  txcls  23428  ptcnp  23446  ufli  23738  tgpt0  23943  tsmsxplem2  23978  nrmmetd  24403  tngngp  24491  tngngp3  24493  reperflem  24654  lebnumlem3  24809  htpyi  24820  htpycc  24826  phtpyi  24830  cfili  25116  cmetcvg  25133  caubl  25156  caublcls  25157  bcthlem2  25173  bcthlem3  25174  bcthlem4  25175  ovolicc2lem1  25366  ovolicc2lem5  25370  ovolicc2  25371  voliunlem3  25401  volsuplem  25404  uniioombllem2  25432  mbfima  25479  ismbfd  25488  ismbf3d  25503  mbfmullem  25575  itg2monolem1  25600  itg2i1fseqle  25604  itg2i1fseq  25605  itg2i1fseq2  25606  itg2addlem  25608  bddmulibl  25688  bddiblnc  25691  c1liplem1  25849  dvfsumle  25874  dvfsumleOLD  25875  dvfsumabs  25877  dvfsumrlimf  25879  dvfsumlem1  25880  dvfsumlem2  25881  dvfsumlem2OLD  25882  dvfsumlem3  25883  dvfsumlem4  25884  dvfsumrlimge0  25885  dvfsum2  25889  ftc1lem6  25896  ulmcau  26246  ulmdvlem1  26251  ulmdvlem3  26253  mtestbdd  26256  itgulm  26259  radcnvlem1  26264  abelthlem5  26287  abelthlem7  26290  areambl  26804  2lgslem1a  27238  dchrisumlem2  27337  dchrvmasumiflem1  27348  pntpbnd1  27433  ostthlem1  27474  madebday  27740  addscom  27797  precsexlem9  28027  tglowdim1i  28186  brbtwn2  28597  ax5seglem1  28620  ax5seglem2  28621  ax5seglem9  28629  axcontlem4  28659  axcontlem12  28667  fusgreghash2wsp  30025  grpoidinvlem3  30193  grpoidinv  30195  grpoidinv2  30202  vcidOLD  30251  minvecolem5  30568  hcaucvg  30873  hlimconvi  30878  lnopeq0i  31694  cnlnadjlem5  31758  csmdsymi  32021  difelsiga  33596  eulerpartlemb  33832  ballotlemfc0  33956  ballotlemfcc  33957  ptpconn  34689  cvmsdisj  34726  cvmshmeo  34727  snmlflim  34788  elmrsubrn  34976  mvtinf  35011  sinccvg  35123  fnemeet1  35717  fnemeet2  35718  fnejoin1  35719  fnejoin2  35720  bj-seex  36268  poimirlem27  36981  poimirlem32  36986  mblfinlem1  36991  ovoliunnfl  36996  ex-ovoliunnfl  36997  voliunnfl  36998  volsupnfl  36999  mbfresfi  37000  itg2gt0cn  37009  ftc1cnnc  37026  ftc1anc  37035  upixp  37063  filbcmb  37074  sdclem1  37077  seqpo  37081  incsequz2  37083  mettrifi  37091  caushft  37095  sstotbnd2  37108  heibor1lem  37143  heiborlem3  37147  heiborlem10  37154  heibor  37155  rrndstprj2  37165  cmpidelt  37193  rngoid  37236  fsuppind  41627  limsuc2  42248  cvgdvgrat  43537  cncmpmax  44181  mccllem  44774  mccl  44775  climinf  44783  climsuse  44785  islptre  44796  limcperiod  44805  addlimc  44825  0ellimcdiv  44826  cncficcgt0  45065  dvbdfbdioolem2  45106  ioodvbdlimc1lem2  45109  ioodvbdlimc2lem  45111  dvnprodlem3  45125  stoweidlem7  45184  stoweidlem15  45192  stoweidlem21  45198  stoweidlem31  45208  stoweidlem35  45212  stoweidlem36  45213  stoweidlem50  45227  stoweidlem57  45234  stoweidlem59  45236  wallispilem3  45244  dirkercncflem2  45281  dirkercncflem4  45283  fourierdlem32  45316  fourierdlem33  45317  fourierdlem39  45323  fourierdlem62  45345  fourierdlem71  45354  fourierdlem89  45372  fourierdlem91  45374  fourierdlem93  45376  fourierdlem101  45384  fourierdlem103  45386  fourierdlem104  45387  etransclem24  45435  etransclem32  45443  smflimlem6  45953  smfpimcc  45985  smfsuplem2  45989  isomushgr  46955