Theorem rspcva 3550

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-2005.)

Hypothesis

Ref	Expression
rspcv.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
rspcva	⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝜑) → 𝜓)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rspcva

Step	Hyp	Ref	Expression
1		rspcv.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
2	1	rspcv 3547	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))
3	2	imp 406	1 ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝜑) → 𝜓)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539   ∈ wcel 2108  ∀wral 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068

This theorem is referenced by:  rexraleqim  3569  fvn0ssdmfun  6934  fveqdmss  6938  fvcofneq  6951  wfr3g  8109  boxriin  8686  boxcutc  8687  marypha1lem  9122  supmo  9141  infmo  9184  unwdomg  9273  frr3g  9445  isinffi  9681  axdc3lem2  10138  grothac  10517  nqereu  10616  nnsub  11947  zextle  12323  xrsupsslem  12970  xrinfmsslem  12971  supxrunb1  12982  supxrunb2  12983  injresinjlem  13435  ssnn0fi  13633  suppssfz  13642  faclbnd4lem4  13938  ishashinf  14105  rexuz3  14988  cau3lem  14994  caubnd2  14997  o1co  15223  climcn1  15229  incexclem  15476  dvdsext  15958  mreintcl  17221  initoeu1  17642  initoeu2  17647  termoeu1  17649  lublecllem  17993  mgmidmo  18259  gsumval2  18285  dfgrp3lem  18588  symgfix2  18939  odeq  19073  gexid  19101  gsummoncoe1  21385  m2detleiblem3  21686  m2detleiblem4  21687  cpmatmcllem  21775  mp2pm2mplem4  21866  cayleyhamilton1  21949  cmpsublem  22458  cmpsub  22459  cmpfii  22468  ptpjcn  22670  isufil2  22967  ufileu  22978  lmmbr  24327  caussi  24366  plyco0  25258  dgrco  25341  emcllem7  26056  isppw2  26169  uvtxnbgrvtx  27663  rusgrnumwwlks  28240  clwwlkf  28312  vdgn1frgrv2  28561  frgrregorufr  28590  grpoidinvlem3  28769  grpoideu  28772  lnconi  30296  fsumiunle  31045  rngurd  31384  tpr2rico  31764  esumiun  31962  0elsiga  31982  sigaclci  32000  dya2icoseg2  32145  derangsn  33032  sat1el2xp  33241  addsid1  34054  fwddifnp1  34394  poimirlem25  35729  poimirlem26  35730  poimirlem30  35734  poimirlem31  35735  poimirlem32  35736  heicant  35739  mblfinlem2  35742  ftc1anc  35785  fdc  35830  bndss  35871  isdrngo2  36043  divrngidl  36113  maxidlmax  36128  cdleme0nex  38231  dihglblem2N  39235  hgmapvs  39832  ismrcd1  40436  nacsfg  40443  isnacs3  40448  nacsfix  40450  mzpcl1  40467  mzpcl2  40468  mzpcong  40710  dnnumch1  40785  aomclem1  40795  aomclem6  40800  lnr2i  40857  hbtlem5  40869  hbt  40871  pwssfi  42482  rexanuz3  42535  choicefi  42629  fsneq  42635  suplesup  42768  xralrple2  42783  infxr  42796  infleinf  42801  xralrple4  42802  xralrple3  42803  xrralrecnnge  42820  supxrunb3  42829  supxrleubrnmpt  42836  unb2ltle  42845  suprleubrnmpt  42852  infxrgelbrnmpt  42884  supminfxr  42894  xrpnf  42916  islpcn  43070  limclner  43082  climd  43103  clim2d  43104  limsupmnflem  43151  limsupre3uzlem  43166  liminflelimsuplem  43206  xlimpnfxnegmnf  43245  xlimxrre  43262  xlimmnfvlem1  43263  xlimmnfv  43265  xlimpnfvlem1  43267  xlimpnfv  43269  climxlim2lem  43276  ioodvbdlimc1lem1  43362  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  fourierdlem103  43640  fourierdlem104  43641  etransclem48  43713  saluncl  43748  subsaliuncllem  43786  sge0pnffigt  43824  omessle  43926  caragensplit  43928  omeunile  43933  hoidmvlelem2  44024  hoidmvlelem3  44025  hoidmvle  44028  vonvolmbllem  44088  vonvolmbl  44089  pimdecfgtioc  44139  smfpreimalt  44154  smfpreimaltf  44159  smfpreimale  44177  smfpreimagt  44184  smfpreimage  44204  smfmullem4  44215  smfinflem  44237  iccpartrn  44770  iccpartiun  44774  icceuelpart  44776  lidldomn1  45367  ply1mulgsumlem2  45616  lindslinindsimp2lem5  45691  lindslinindsimp2  45692  snlindsntor  45700  nn0sumshdiglemA  45853  nn0sumshdiglemB  45854  nn0sumshdig  45857