Theorem rspcva 3633

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2108  ∀wral 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068

This theorem is referenced by:  rexraleqim  3660  fvn0ssdmfun  7108  fveqdmss  7112  fvcofneq  7127  wfr3g  8363  boxriin  8998  boxcutc  8999  marypha1lem  9502  supmo  9521  infmo  9564  unwdomg  9653  frr3g  9825  isinffi  10061  axdc3lem2  10520  grothac  10899  nqereu  10998  nnsub  12337  zextle  12716  xrsupsslem  13369  xrinfmsslem  13370  supxrunb1  13381  supxrunb2  13382  injresinjlem  13837  ssnn0fi  14036  suppssfz  14045  faclbnd4lem4  14345  ishashinf  14512  rexuz3  15397  cau3lem  15403  caubnd2  15406  o1co  15632  climcn1  15638  incexclem  15884  dvdsext  16369  mreintcl  17653  initoeu1  18078  initoeu2  18083  termoeu1  18085  lublecllem  18430  mgmidmo  18698  gsumval2  18724  dfgrp3lem  19078  symgfix2  19458  odeq  19592  gexid  19623  ringurd  20212  o2timesd  20237  rglcom4d  20238  gsummoncoe1  22333  m2detleiblem3  22656  m2detleiblem4  22657  cpmatmcllem  22745  mp2pm2mplem4  22836  cayleyhamilton1  22919  cmpsublem  23428  cmpsub  23429  cmpfii  23438  ptpjcn  23640  isufil2  23937  ufileu  23948  lmmbr  25311  caussi  25350  plyco0  26251  dgrco  26335  emcllem7  27063  isppw2  27176  addsrid  28015  mulsrid  28157  n0subs  28378  uvtxnbgrvtx  29428  rusgrnumwwlks  30007  clwwlkf  30079  vdgn1frgrv2  30328  frgrregorufr  30357  grpoidinvlem3  30538  grpoideu  30541  lnconi  32065  fsumiunle  32833  tpr2rico  33858  esumiun  34058  0elsiga  34078  sigaclci  34096  dya2icoseg2  34243  derangsn  35138  sat1el2xp  35347  fwddifnp1  36129  poimirlem25  37605  poimirlem26  37606  poimirlem30  37610  poimirlem31  37611  poimirlem32  37612  heicant  37615  mblfinlem2  37618  ftc1anc  37661  fdc  37705  bndss  37746  isdrngo2  37918  divrngidl  37988  maxidlmax  38003  cdleme0nex  40247  dihglblem2N  41251  hgmapvs  41848  ismrcd1  42654  nacsfg  42661  isnacs3  42666  nacsfix  42668  mzpcl1  42685  mzpcl2  42686  mzpcong  42929  dnnumch1  43001  aomclem1  43011  aomclem6  43016  lnr2i  43073  hbtlem5  43085  hbt  43087  pwssfi  44947  rexanuz3  44998  choicefi  45107  fsneq  45113  suplesup  45254  xralrple2  45269  infxr  45282  infleinf  45287  xralrple4  45288  xralrple3  45289  xrralrecnnge  45305  supxrunb3  45314  supxrleubrnmpt  45321  unb2ltle  45330  suprleubrnmpt  45337  infxrgelbrnmpt  45369  supminfxr  45379  xrpnf  45401  islpcn  45560  limclner  45572  climd  45593  clim2d  45594  limsupmnflem  45641  limsupre3uzlem  45656  liminflelimsuplem  45696  xlimpnfxnegmnf  45735  xlimxrre  45752  xlimmnfvlem1  45753  xlimmnfv  45755  xlimpnfvlem1  45757  xlimpnfv  45759  climxlim2lem  45766  ioodvbdlimc1lem1  45852  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  fourierdlem103  46130  fourierdlem104  46131  etransclem48  46203  saluncl  46238  subsaliuncllem  46278  sge0pnffigt  46317  omessle  46419  caragensplit  46421  omeunile  46426  hoidmvlelem2  46517  hoidmvlelem3  46518  hoidmvle  46521  vonvolmbllem  46581  vonvolmbl  46582  pimdecfgtioc  46636  smfpreimalt  46652  smfpreimaltf  46657  smfpreimale  46675  smfpreimagt  46683  smfpreimage  46703  smfmullem4  46715  smfinflem  46738  iccpartrn  47304  iccpartiun  47308  icceuelpart  47310  lidldomn1  47954  ply1mulgsumlem2  48116  lindslinindsimp2lem5  48191  lindslinindsimp2  48192  snlindsntor  48200  nn0sumshdiglemA  48353  nn0sumshdiglemB  48354  nn0sumshdig  48357