Theorem rspccva 3510

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   = wceq 1601   ∈ wcel 2107  ∀wral 3090

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-v 3400

This theorem is referenced by:  disjne  4247  n0snor2el  4595  seex  5320  preddowncl  5962  foelrn  6644  grprinvlem  7151  caofid0l  7204  caofid0r  7205  caofid1  7206  caofid2  7207  onnseq  7726  odi  7945  omsmolem  8019  fvixp  8201  unblem1  8502  ordiso2  8711  unwdomg  8780  ac5num  9194  acni2  9204  fodomacn  9214  iundom2g  9699  fpwwe2lem3  9792  eltsk2g  9910  tskpwss  9911  tskpw  9912  tsken  9913  prlem934  10192  dedekindle  10542  ltord1  10904  leord1  10905  eqord1  10906  ltord2  10907  leord2  10908  eqord2  10909  supmul1  11351  seqcaopr2  13160  bccl  13433  hashbc  13557  limsupbnd2  14631  2clim  14720  climsup  14817  caurcvg2  14825  caucvgb  14827  isummulc2  14907  telfsumo2  14948  fsumparts  14951  incexclem  14981  isumshft  14984  climcndslem1  14994  climcndslem2  14995  supcvg  15001  geomulcvg  15020  mertenslem2  15029  mertens  15030  bpolycl  15194  bpolydif  15197  rpnnen2lem10  15365  dvdsprime  15816  fuciso  17031  lubub  17516  lubl  17517  mgmlrid  17663  grpinvex  17830  issubg2  18004  issubg4  18008  nmzbi  18029  gagrpid  18121  cntzi  18156  psgnunilem2  18310  sylow1lem3  18410  pgpfi  18415  slwispgp  18421  sylow2alem1  18427  dprdfcl  18810  ablfac2  18886  abveq0  19229  issrngd  19264  psrbagconf1o  19782  pf1ind  20126  phllmhm  20386  ipcl  20387  ipeq0  20392  isphld  20408  ocvi  20423  cayhamlem3  21110  elcls3  21306  neindisj2  21346  perfi  21378  cnima  21488  1stcfb  21668  1stcelcls  21684  llyi  21697  nllyi  21698  locfinnei  21746  1stckgenlem  21776  ptbasin  21800  txcls  21827  ptcnp  21845  ufli  22137  tgpt0  22341  tsmsxplem2  22376  nrmmetd  22798  tngngp  22877  tngngp3  22879  reperflem  23040  lebnumlem3  23181  htpyi  23192  htpycc  23198  phtpyi  23202  cfili  23485  cmetcvg  23502  caubl  23525  caublcls  23526  bcthlem2  23542  bcthlem3  23543  bcthlem4  23544  ovolicc2lem1  23732  ovolicc2lem5  23736  ovolicc2  23737  voliunlem3  23767  volsuplem  23770  uniioombllem2  23798  mbfima  23845  ismbfd  23854  ismbf3d  23869  mbfmullem  23940  itg2monolem1  23965  itg2i1fseqle  23969  itg2i1fseq  23970  itg2i1fseq2  23971  itg2addlem  23973  bddmulibl  24053  c1liplem1  24207  dvfsumle  24232  dvfsumabs  24234  dvfsumrlimf  24236  dvfsumlem1  24237  dvfsumlem2  24238  dvfsumlem3  24239  dvfsumlem4  24240  dvfsumrlimge0  24241  dvfsum2  24245  ftc1lem6  24252  ulmcau  24597  ulmdvlem1  24602  ulmdvlem3  24604  mtestbdd  24607  itgulm  24610  radcnvlem1  24615  abelthlem5  24637  abelthlem7  24640  areambl  25148  2lgslem1a  25579  dchrisumlem2  25648  dchrvmasumiflem1  25659  pntpbnd1  25744  ostthlem1  25785  tglowdim1i  25869  brbtwn2  26271  ax5seglem1  26294  ax5seglem2  26295  ax5seglem9  26303  axcontlem4  26333  axcontlem12  26341  0vtxrusgr  26942  fusgreghash2wsp  27763  grpoidinvlem3  27950  grpoidinv  27952  grpoidinv2  27959  vcidOLD  28008  minvecolem5  28326  hcaucvg  28632  hlimconvi  28637  lnopeq0i  29455  cnlnadjlem5  29519  csmdsymi  29782  difelsiga  30802  eulerpartlemb  31036  ballotlemfc0  31161  ballotlemfcc  31162  ptpconn  31822  cvmsdisj  31859  cvmshmeo  31860  snmlflim  31921  elmrsubrn  32024  mvtinf  32059  sinccvg  32172  fnemeet1  32957  fnemeet2  32958  fnejoin1  32959  fnejoin2  32960  bj-seex  33500  poimirlem27  34071  poimirlem32  34076  mblfinlem1  34081  ovoliunnfl  34086  ex-ovoliunnfl  34087  voliunnfl  34088  volsupnfl  34089  mbfresfi  34090  itg2gt0cn  34099  bddiblnc  34114  ftc1cnnc  34118  ftc1anc  34127  upixp  34158  filbcmb  34169  sdclem1  34172  seqpo  34176  incsequz2  34178  mettrifi  34186  caushft  34190  sstotbnd2  34206  heibor1lem  34241  heiborlem3  34245  heiborlem10  34252  heibor  34253  rrndstprj2  34263  cmpidelt  34291  rngoid  34334  limsuc2  38584  cvgdvgrat  39482  cncmpmax  40138  foelrnf  40310  mccllem  40751  mccl  40752  climinf  40760  climsuse  40762  islptre  40773  limcperiod  40782  addlimc  40802  0ellimcdiv  40803  cncficcgt0  41043  dvbdfbdioolem2  41086  ioodvbdlimc1lem2  41089  ioodvbdlimc2lem  41091  dvnprodlem3  41105  stoweidlem7  41165  stoweidlem15  41173  stoweidlem21  41179  stoweidlem31  41189  stoweidlem35  41193  stoweidlem36  41194  stoweidlem50  41208  stoweidlem57  41215  stoweidlem59  41217  wallispilem3  41225  dirkercncflem2  41262  dirkercncflem4  41264  fourierdlem32  41297  fourierdlem33  41298  fourierdlem39  41304  fourierdlem62  41326  fourierdlem71  41335  fourierdlem89  41353  fourierdlem91  41355  fourierdlem93  41357  fourierdlem101  41365  fourierdlem103  41367  fourierdlem104  41368  etransclem24  41416  etransclem32  41424  smflimlem6  41925  smfpimcc  41955  smfsuplem2  41959  isomushgr  42753