Theorem rspccva 3584

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ 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-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045

This theorem is referenced by:  disjne  4414  n0snor2el  4793  seex  5590  preddowncl  6293  frpoins3g  6307  foelrn  7061  foelrnf  7062  caofid0l  7666  caofid0r  7667  caofid1  7668  caofid2  7669  onnseq  8290  odi  8520  omsmolem  8598  naddssim  8626  fvixp  8852  unblem1  9215  ordiso2  9444  unwdomg  9513  ac5num  9965  acni2  9975  fodomacn  9985  iundom2g  10469  fpwwe2lem3  10562  eltsk2g  10680  tskpwss  10681  tskpw  10682  tsken  10683  prlem934  10962  dedekindle  11314  ltord1  11680  leord1  11681  eqord1  11682  ltord2  11683  leord2  11684  eqord2  11685  supmul1  12128  seqcaopr2  13979  bccl  14263  hashbc  14394  limsupbnd2  15425  2clim  15514  climsup  15612  caurcvg2  15620  caucvgb  15622  isummulc2  15704  telfsumo2  15745  fsumparts  15748  incexclem  15778  isumshft  15781  climcndslem1  15791  climcndslem2  15792  supcvg  15798  geomulcvg  15818  mertenslem2  15827  mertens  15828  bpolycl  15994  bpolydif  15997  rpnnen2lem10  16167  dvdsprime  16633  fuciso  17920  lubub  18452  lubl  18453  mgmlrid  18576  grpinvalem  18582  grpinvex  18857  issubg2  19055  issubg4  19059  nmzbi  19078  gagrpid  19208  cntzi  19243  psgnunilem2  19409  sylow1lem3  19514  pgpfi  19519  slwispgp  19525  sylow2alem1  19531  dprdfcl  19929  ablfac2  20005  abveq0  20738  issrngd  20775  phllmhm  21574  ipcl  21575  ipeq0  21580  isphld  21596  ocvi  21611  pf1ind  22275  cayhamlem3  22807  elcls3  23003  neindisj2  23043  perfi  23075  cnima  23185  1stcfb  23365  1stcelcls  23381  llyi  23394  nllyi  23395  locfinnei  23443  1stckgenlem  23473  ptbasin  23497  txcls  23524  ptcnp  23542  ufli  23834  tgpt0  24039  tsmsxplem2  24074  nrmmetd  24495  tngngp  24575  tngngp3  24577  reperflem  24740  lebnumlem3  24895  htpyi  24906  htpycc  24912  phtpyi  24916  cfili  25201  cmetcvg  25218  caubl  25241  caublcls  25242  bcthlem2  25258  bcthlem3  25259  bcthlem4  25260  ovolicc2lem1  25451  ovolicc2lem5  25455  ovolicc2  25456  voliunlem3  25486  volsuplem  25489  uniioombllem2  25517  mbfima  25564  ismbfd  25573  ismbf3d  25588  mbfmullem  25659  itg2monolem1  25684  itg2i1fseqle  25688  itg2i1fseq  25689  itg2i1fseq2  25690  itg2addlem  25692  bddmulibl  25773  bddiblnc  25776  c1liplem1  25934  dvfsumle  25959  dvfsumleOLD  25960  dvfsumabs  25962  dvfsumrlimf  25964  dvfsumlem1  25965  dvfsumlem2  25966  dvfsumlem2OLD  25967  dvfsumlem3  25968  dvfsumlem4  25969  dvfsumrlimge0  25970  dvfsum2  25974  ftc1lem6  25981  ulmcau  26337  ulmdvlem1  26342  ulmdvlem3  26344  mtestbdd  26347  itgulm  26350  radcnvlem1  26355  abelthlem5  26378  abelthlem7  26381  areambl  26901  2lgslem1a  27335  dchrisumlem2  27434  dchrvmasumiflem1  27445  pntpbnd1  27530  ostthlem1  27571  madebday  27849  addscom  27913  precsexlem9  28157  peano5n0s  28252  zs12bday  28396  tglowdim1i  28481  brbtwn2  28885  ax5seglem1  28908  ax5seglem2  28909  ax5seglem9  28917  axcontlem4  28947  axcontlem12  28955  fusgreghash2wsp  30317  grpoidinvlem3  30485  grpoidinv  30487  grpoidinv2  30494  vcidOLD  30543  minvecolem5  30860  hcaucvg  31165  hlimconvi  31170  lnopeq0i  31986  cnlnadjlem5  32050  csmdsymi  32313  difelsiga  34116  eulerpartlemb  34352  ballotlemfc0  34477  ballotlemfcc  34478  ptpconn  35213  cvmsdisj  35250  cvmshmeo  35251  snmlflim  35312  elmrsubrn  35500  mvtinf  35535  sinccvg  35653  fnemeet1  36347  fnemeet2  36348  fnejoin1  36349  fnejoin2  36350  bj-seex  36903  poimirlem27  37634  poimirlem32  37639  mblfinlem1  37644  ovoliunnfl  37649  ex-ovoliunnfl  37650  voliunnfl  37651  volsupnfl  37652  mbfresfi  37653  itg2gt0cn  37662  ftc1cnnc  37679  ftc1anc  37688  upixp  37716  filbcmb  37727  sdclem1  37730  seqpo  37734  incsequz2  37736  mettrifi  37744  caushft  37748  sstotbnd2  37761  heibor1lem  37796  heiborlem3  37800  heiborlem10  37807  heibor  37808  rrndstprj2  37818  cmpidelt  37846  rngoid  37889  fsuppind  42571  limsuc2  43023  cvgdvgrat  44295  cncmpmax  45019  mccllem  45588  mccl  45589  climinf  45597  climsuse  45599  islptre  45610  limcperiod  45619  addlimc  45639  0ellimcdiv  45640  cncficcgt0  45879  dvbdfbdioolem2  45920  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  dvnprodlem3  45939  stoweidlem7  45998  stoweidlem15  46006  stoweidlem21  46012  stoweidlem31  46022  stoweidlem35  46026  stoweidlem36  46027  stoweidlem50  46041  stoweidlem57  46048  stoweidlem59  46050  wallispilem3  46058  dirkercncflem2  46095  dirkercncflem4  46097  fourierdlem32  46130  fourierdlem33  46131  fourierdlem39  46137  fourierdlem62  46159  fourierdlem71  46168  fourierdlem89  46186  fourierdlem91  46188  fourierdlem93  46190  fourierdlem101  46198  fourierdlem103  46200  fourierdlem104  46201  etransclem24  46249  etransclem32  46257  smflimlem6  46767  smfpimcc  46799  smfsuplem2  46803  gricushgr  47910