Theorem rspccva 3575

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∀wral 3051

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052

This theorem is referenced by:  disjne  4407  n0snor2el  4789  seex  5583  preddowncl  6290  frpoins3g  6304  foelrn  7052  foelrnf  7053  caofid0l  7655  caofid0r  7656  caofid1  7657  caofid2  7658  onnseq  8276  odi  8506  omsmolem  8585  naddssim  8613  fvixp  8840  unblem1  9192  ordiso2  9420  unwdomg  9489  ac5num  9946  acni2  9956  fodomacn  9966  iundom2g  10450  fpwwe2lem3  10544  eltsk2g  10662  tskpwss  10663  tskpw  10664  tsken  10665  prlem934  10944  dedekindle  11297  ltord1  11663  leord1  11664  eqord1  11665  ltord2  11666  leord2  11667  eqord2  11668  supmul1  12111  seqcaopr2  13961  bccl  14245  hashbc  14376  limsupbnd2  15406  2clim  15495  climsup  15593  caurcvg2  15601  caucvgb  15603  isummulc2  15685  telfsumo2  15726  fsumparts  15729  incexclem  15759  isumshft  15762  climcndslem1  15772  climcndslem2  15773  supcvg  15779  geomulcvg  15799  mertenslem2  15808  mertens  15809  bpolycl  15975  bpolydif  15978  rpnnen2lem10  16148  dvdsprime  16614  fuciso  17902  lubub  18434  lubl  18435  mgmlrid  18592  grpinvalem  18598  grpinvex  18873  issubg2  19071  issubg4  19075  nmzbi  19093  gagrpid  19223  cntzi  19258  psgnunilem2  19424  sylow1lem3  19529  pgpfi  19534  slwispgp  19540  sylow2alem1  19546  dprdfcl  19944  ablfac2  20020  abveq0  20751  issrngd  20788  phllmhm  21587  ipcl  21588  ipeq0  21593  isphld  21609  ocvi  21624  pf1ind  22299  cayhamlem3  22831  elcls3  23027  neindisj2  23067  perfi  23099  cnima  23209  1stcfb  23389  1stcelcls  23405  llyi  23418  nllyi  23419  locfinnei  23467  1stckgenlem  23497  ptbasin  23521  txcls  23548  ptcnp  23566  ufli  23858  tgpt0  24063  tsmsxplem2  24098  nrmmetd  24518  tngngp  24598  tngngp3  24600  reperflem  24763  lebnumlem3  24918  htpyi  24929  htpycc  24935  phtpyi  24939  cfili  25224  cmetcvg  25241  caubl  25264  caublcls  25265  bcthlem2  25281  bcthlem3  25282  bcthlem4  25283  ovolicc2lem1  25474  ovolicc2lem5  25478  ovolicc2  25479  voliunlem3  25509  volsuplem  25512  uniioombllem2  25540  mbfima  25587  ismbfd  25596  ismbf3d  25611  mbfmullem  25682  itg2monolem1  25707  itg2i1fseqle  25711  itg2i1fseq  25712  itg2i1fseq2  25713  itg2addlem  25715  bddmulibl  25796  bddiblnc  25799  c1liplem1  25957  dvfsumle  25982  dvfsumleOLD  25983  dvfsumabs  25985  dvfsumrlimf  25987  dvfsumlem1  25988  dvfsumlem2  25989  dvfsumlem2OLD  25990  dvfsumlem3  25991  dvfsumlem4  25992  dvfsumrlimge0  25993  dvfsum2  25997  ftc1lem6  26004  ulmcau  26360  ulmdvlem1  26365  ulmdvlem3  26367  mtestbdd  26370  itgulm  26373  radcnvlem1  26378  abelthlem5  26401  abelthlem7  26404  areambl  26924  2lgslem1a  27358  dchrisumlem2  27457  dchrvmasumiflem1  27468  pntpbnd1  27553  ostthlem1  27594  madebday  27896  addscom  27962  precsexlem9  28211  peano5n0s  28315  bdayfinbndlem1  28463  tglowdim1i  28573  brbtwn2  28978  ax5seglem1  29001  ax5seglem2  29002  ax5seglem9  29010  axcontlem4  29040  axcontlem12  29048  fusgreghash2wsp  30413  grpoidinvlem3  30581  grpoidinv  30583  grpoidinv2  30590  vcidOLD  30639  minvecolem5  30956  hcaucvg  31261  hlimconvi  31266  lnopeq0i  32082  cnlnadjlem5  32146  csmdsymi  32409  difelsiga  34290  eulerpartlemb  34525  ballotlemfc0  34650  ballotlemfcc  34651  ptpconn  35427  cvmsdisj  35464  cvmshmeo  35465  snmlflim  35526  elmrsubrn  35714  mvtinf  35749  sinccvg  35867  fnemeet1  36560  fnemeet2  36561  fnejoin1  36562  fnejoin2  36563  bj-seex  37123  poimirlem27  37848  poimirlem32  37853  mblfinlem1  37858  ovoliunnfl  37863  ex-ovoliunnfl  37864  voliunnfl  37865  volsupnfl  37866  mbfresfi  37867  itg2gt0cn  37876  ftc1cnnc  37893  ftc1anc  37902  upixp  37930  filbcmb  37941  sdclem1  37944  seqpo  37948  incsequz2  37950  mettrifi  37958  caushft  37962  sstotbnd2  37975  heibor1lem  38010  heiborlem3  38014  heiborlem10  38021  heibor  38022  rrndstprj2  38032  cmpidelt  38060  rngoid  38103  fsuppind  42833  limsuc2  43283  cvgdvgrat  44554  cncmpmax  45277  mccllem  45843  mccl  45844  climinf  45852  climsuse  45854  islptre  45865  limcperiod  45874  addlimc  45892  0ellimcdiv  45893  cncficcgt0  46132  dvbdfbdioolem2  46173  ioodvbdlimc1lem2  46176  ioodvbdlimc2lem  46178  dvnprodlem3  46192  stoweidlem7  46251  stoweidlem15  46259  stoweidlem21  46265  stoweidlem31  46275  stoweidlem35  46279  stoweidlem36  46280  stoweidlem50  46294  stoweidlem57  46301  stoweidlem59  46303  wallispilem3  46311  dirkercncflem2  46348  dirkercncflem4  46350  fourierdlem32  46383  fourierdlem33  46384  fourierdlem39  46390  fourierdlem62  46412  fourierdlem71  46421  fourierdlem89  46439  fourierdlem91  46441  fourierdlem93  46443  fourierdlem101  46451  fourierdlem103  46453  fourierdlem104  46454  etransclem24  46502  etransclem32  46510  smflimlem6  47020  smfpimcc  47052  smfsuplem2  47056  gricushgr  48163