Theorem rspccva 3564

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053

This theorem is referenced by:  disjne  4396  n0snor2el  4777  seex  5584  preddowncl  6291  frpoins3g  6305  foelrn  7054  foelrnf  7055  caofid0l  7658  caofid0r  7659  caofid1  7660  caofid2  7661  onnseq  8278  odi  8508  omsmolem  8587  naddssim  8615  fvixp  8844  unblem1  9196  ordiso2  9424  unwdomg  9493  ac5num  9952  acni2  9962  fodomacn  9972  iundom2g  10456  fpwwe2lem3  10550  eltsk2g  10668  tskpwss  10669  tskpw  10670  tsken  10671  prlem934  10950  dedekindle  11304  ltord1  11670  leord1  11671  eqord1  11672  ltord2  11673  leord2  11674  eqord2  11675  supmul1  12119  seqcaopr2  13994  bccl  14278  hashbc  14409  limsupbnd2  15439  2clim  15528  climsup  15626  caurcvg2  15634  caucvgb  15636  isummulc2  15718  telfsumo2  15760  fsumparts  15763  incexclem  15795  isumshft  15798  climcndslem1  15808  climcndslem2  15809  supcvg  15815  geomulcvg  15835  mertenslem2  15844  mertens  15845  bpolycl  16011  bpolydif  16014  rpnnen2lem10  16184  dvdsprime  16650  fuciso  17939  lubub  18471  lubl  18472  mgmlrid  18629  grpinvalem  18635  grpinvex  18913  issubg2  19111  issubg4  19115  nmzbi  19133  gagrpid  19263  cntzi  19298  psgnunilem2  19464  sylow1lem3  19569  pgpfi  19574  slwispgp  19580  sylow2alem1  19586  dprdfcl  19984  ablfac2  20060  abveq0  20789  issrngd  20826  phllmhm  21625  ipcl  21626  ipeq0  21631  isphld  21647  ocvi  21662  pf1ind  22333  cayhamlem3  22865  elcls3  23061  neindisj2  23101  perfi  23133  cnima  23243  1stcfb  23423  1stcelcls  23439  llyi  23452  nllyi  23453  locfinnei  23501  1stckgenlem  23531  ptbasin  23555  txcls  23582  ptcnp  23600  ufli  23892  tgpt0  24097  tsmsxplem2  24132  nrmmetd  24552  tngngp  24632  tngngp3  24634  reperflem  24797  lebnumlem3  24943  htpyi  24954  htpycc  24960  phtpyi  24964  cfili  25248  cmetcvg  25265  caubl  25288  caublcls  25289  bcthlem2  25305  bcthlem3  25306  bcthlem4  25307  ovolicc2lem1  25497  ovolicc2lem5  25501  ovolicc2  25502  voliunlem3  25532  volsuplem  25535  uniioombllem2  25563  mbfima  25610  ismbfd  25619  ismbf3d  25634  mbfmullem  25705  itg2monolem1  25730  itg2i1fseqle  25734  itg2i1fseq  25735  itg2i1fseq2  25736  itg2addlem  25738  bddmulibl  25819  bddiblnc  25822  c1liplem1  25976  dvfsumle  26001  dvfsumabs  26003  dvfsumrlimf  26005  dvfsumlem1  26006  dvfsumlem2  26007  dvfsumlem3  26008  dvfsumlem4  26009  dvfsumrlimge0  26010  dvfsum2  26014  ftc1lem6  26021  ulmcau  26376  ulmdvlem1  26381  ulmdvlem3  26383  mtestbdd  26386  itgulm  26389  radcnvlem1  26394  abelthlem5  26416  abelthlem7  26419  areambl  26938  2lgslem1a  27371  dchrisumlem2  27470  dchrvmasumiflem1  27481  pntpbnd1  27566  ostthlem1  27607  madebday  27909  addscom  27975  precsexlem9  28224  peano5n0s  28328  bdayfinbndlem1  28476  tglowdim1i  28586  brbtwn2  28991  ax5seglem1  29014  ax5seglem2  29015  ax5seglem9  29023  axcontlem4  29053  axcontlem12  29061  fusgreghash2wsp  30426  grpoidinvlem3  30595  grpoidinv  30597  grpoidinv2  30604  vcidOLD  30653  minvecolem5  30970  hcaucvg  31275  hlimconvi  31280  lnopeq0i  32096  cnlnadjlem5  32160  csmdsymi  32423  difelsiga  34296  eulerpartlemb  34531  ballotlemfc0  34656  ballotlemfcc  34657  ptpconn  35434  cvmsdisj  35471  cvmshmeo  35472  snmlflim  35533  elmrsubrn  35721  mvtinf  35756  sinccvg  35874  fnemeet1  36567  fnemeet2  36568  fnejoin1  36569  fnejoin2  36570  bj-seex  37248  poimirlem27  37985  poimirlem32  37990  mblfinlem1  37995  ovoliunnfl  38000  ex-ovoliunnfl  38001  voliunnfl  38002  volsupnfl  38003  mbfresfi  38004  itg2gt0cn  38013  ftc1cnnc  38030  ftc1anc  38039  upixp  38067  filbcmb  38078  sdclem1  38081  seqpo  38085  incsequz2  38087  mettrifi  38095  caushft  38099  sstotbnd2  38112  heibor1lem  38147  heiborlem3  38151  heiborlem10  38158  heibor  38159  rrndstprj2  38169  cmpidelt  38197  rngoid  38240  fsuppind  43040  limsuc2  43490  cvgdvgrat  44761  cncmpmax  45484  mccllem  46048  mccl  46049  climinf  46057  climsuse  46059  islptre  46070  limcperiod  46079  addlimc  46097  0ellimcdiv  46098  cncficcgt0  46337  dvbdfbdioolem2  46378  ioodvbdlimc1lem2  46381  ioodvbdlimc2lem  46383  dvnprodlem3  46397  stoweidlem7  46456  stoweidlem15  46464  stoweidlem21  46470  stoweidlem31  46480  stoweidlem35  46484  stoweidlem36  46485  stoweidlem50  46499  stoweidlem57  46506  stoweidlem59  46508  wallispilem3  46516  dirkercncflem2  46553  dirkercncflem4  46555  fourierdlem32  46588  fourierdlem33  46589  fourierdlem39  46595  fourierdlem62  46617  fourierdlem71  46626  fourierdlem89  46644  fourierdlem91  46646  fourierdlem93  46648  fourierdlem101  46656  fourierdlem103  46658  fourierdlem104  46659  etransclem24  46707  etransclem32  46715  smflimlem6  47225  smfpimcc  47257  smfsuplem2  47261  gricushgr  48408