Theorem rspccva 3526

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1543   ∈ wcel 2112  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-ral 3056

This theorem is referenced by:  disjne  4355  n0snor2el  4730  seex  5498  preddowncl  6168  frpoins3g  6178  foelrn  6903  caofid0l  7477  caofid0r  7478  caofid1  7479  caofid2  7480  onnseq  8059  odi  8285  omsmolem  8360  fvixp  8561  unblem1  8901  ordiso2  9109  unwdomg  9178  ac5num  9615  acni2  9625  fodomacn  9635  iundom2g  10119  fpwwe2lem3  10212  eltsk2g  10330  tskpwss  10331  tskpw  10332  tsken  10333  prlem934  10612  dedekindle  10961  ltord1  11323  leord1  11324  eqord1  11325  ltord2  11326  leord2  11327  eqord2  11328  supmul1  11766  seqcaopr2  13577  bccl  13853  hashbc  13982  limsupbnd2  15009  2clim  15098  climsup  15198  caurcvg2  15206  caucvgb  15208  isummulc2  15289  telfsumo2  15330  fsumparts  15333  incexclem  15363  isumshft  15366  climcndslem1  15376  climcndslem2  15377  supcvg  15383  geomulcvg  15403  mertenslem2  15412  mertens  15413  bpolycl  15577  bpolydif  15580  rpnnen2lem10  15747  dvdsprime  16207  fuciso  17438  lubub  17971  lubl  17972  mgmlrid  18093  grprinvlem  18099  grpinvex  18329  issubg2  18512  issubg4  18516  nmzbi  18534  gagrpid  18642  cntzi  18677  psgnunilem2  18841  sylow1lem3  18943  pgpfi  18948  slwispgp  18954  sylow2alem1  18960  dprdfcl  19354  ablfac2  19430  abveq0  19816  issrngd  19851  phllmhm  20548  ipcl  20549  ipeq0  20554  isphld  20570  ocvi  20585  psrbagconf1oOLD  20850  pf1ind  21225  cayhamlem3  21738  elcls3  21934  neindisj2  21974  perfi  22006  cnima  22116  1stcfb  22296  1stcelcls  22312  llyi  22325  nllyi  22326  locfinnei  22374  1stckgenlem  22404  ptbasin  22428  txcls  22455  ptcnp  22473  ufli  22765  tgpt0  22970  tsmsxplem2  23005  nrmmetd  23426  tngngp  23506  tngngp3  23508  reperflem  23669  lebnumlem3  23814  htpyi  23825  htpycc  23831  phtpyi  23835  cfili  24119  cmetcvg  24136  caubl  24159  caublcls  24160  bcthlem2  24176  bcthlem3  24177  bcthlem4  24178  ovolicc2lem1  24368  ovolicc2lem5  24372  ovolicc2  24373  voliunlem3  24403  volsuplem  24406  uniioombllem2  24434  mbfima  24481  ismbfd  24490  ismbf3d  24505  mbfmullem  24577  itg2monolem1  24602  itg2i1fseqle  24606  itg2i1fseq  24607  itg2i1fseq2  24608  itg2addlem  24610  bddmulibl  24690  bddiblnc  24693  c1liplem1  24847  dvfsumle  24872  dvfsumabs  24874  dvfsumrlimf  24876  dvfsumlem1  24877  dvfsumlem2  24878  dvfsumlem3  24879  dvfsumlem4  24880  dvfsumrlimge0  24881  dvfsum2  24885  ftc1lem6  24892  ulmcau  25241  ulmdvlem1  25246  ulmdvlem3  25248  mtestbdd  25251  itgulm  25254  radcnvlem1  25259  abelthlem5  25281  abelthlem7  25284  areambl  25795  2lgslem1a  26226  dchrisumlem2  26325  dchrvmasumiflem1  26336  pntpbnd1  26421  ostthlem1  26462  tglowdim1i  26546  brbtwn2  26950  ax5seglem1  26973  ax5seglem2  26974  ax5seglem9  26982  axcontlem4  27012  axcontlem12  27020  fusgreghash2wsp  28375  grpoidinvlem3  28541  grpoidinv  28543  grpoidinv2  28550  vcidOLD  28599  minvecolem5  28916  hcaucvg  29221  hlimconvi  29226  lnopeq0i  30042  cnlnadjlem5  30106  csmdsymi  30369  difelsiga  31767  eulerpartlemb  32001  ballotlemfc0  32125  ballotlemfcc  32126  ptpconn  32862  cvmsdisj  32899  cvmshmeo  32900  snmlflim  32961  elmrsubrn  33149  mvtinf  33184  sinccvg  33298  naddssim  33523  madebday  33766  addscom  33815  fnemeet1  34241  fnemeet2  34242  fnejoin1  34243  fnejoin2  34244  bj-seex  34797  poimirlem27  35490  poimirlem32  35495  mblfinlem1  35500  ovoliunnfl  35505  ex-ovoliunnfl  35506  voliunnfl  35507  volsupnfl  35508  mbfresfi  35509  itg2gt0cn  35518  ftc1cnnc  35535  ftc1anc  35544  upixp  35573  filbcmb  35584  sdclem1  35587  seqpo  35591  incsequz2  35593  mettrifi  35601  caushft  35605  sstotbnd2  35618  heibor1lem  35653  heiborlem3  35657  heiborlem10  35664  heibor  35665  rrndstprj2  35675  cmpidelt  35703  rngoid  35746  fsuppind  39930  limsuc2  40510  cvgdvgrat  41545  cncmpmax  42189  foelrnf  42338  mccllem  42756  mccl  42757  climinf  42765  climsuse  42767  islptre  42778  limcperiod  42787  addlimc  42807  0ellimcdiv  42808  cncficcgt0  43047  dvbdfbdioolem2  43088  ioodvbdlimc1lem2  43091  ioodvbdlimc2lem  43093  dvnprodlem3  43107  stoweidlem7  43166  stoweidlem15  43174  stoweidlem21  43180  stoweidlem31  43190  stoweidlem35  43194  stoweidlem36  43195  stoweidlem50  43209  stoweidlem57  43216  stoweidlem59  43218  wallispilem3  43226  dirkercncflem2  43263  dirkercncflem4  43265  fourierdlem32  43298  fourierdlem33  43299  fourierdlem39  43305  fourierdlem62  43327  fourierdlem71  43336  fourierdlem89  43354  fourierdlem91  43356  fourierdlem93  43358  fourierdlem101  43366  fourierdlem103  43368  fourierdlem104  43369  etransclem24  43417  etransclem32  43425  smflimlem6  43926  smfpimcc  43956  smfsuplem2  43960  isomushgr  44894