Theorem rspcva 3624

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1536   ∈ wcel 2113  ∀wral 3141

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-cleq 2817  df-clel 2896  df-ral 3146

This theorem is referenced by:  rexraleqim  3643  fvn0ssdmfun  6845  fveqdmss  6849  fvcofneq  6862  wfr3g  7956  boxriin  8507  boxcutc  8508  marypha1lem  8900  supmo  8919  infmo  8962  unwdomg  9051  isinffi  9424  axdc3lem2  9876  grothac  10255  nqereu  10354  nnsub  11684  zextle  12058  xrsupsslem  12703  xrinfmsslem  12704  supxrunb1  12715  supxrunb2  12716  injresinjlem  13160  ssnn0fi  13356  suppssfz  13365  faclbnd4lem4  13659  ishashinf  13824  rexuz3  14711  cau3lem  14717  caubnd2  14720  o1co  14946  climcn1  14951  incexclem  15194  dvdsext  15674  mreintcl  16869  initoeu1  17274  initoeu2  17279  termoeu1  17281  lublecllem  17601  mgmidmo  17873  gsumval2  17899  dfgrp3lem  18200  symgfix2  18547  odeq  18681  gexid  18709  gsummoncoe1  20475  m2detleiblem3  21241  m2detleiblem4  21242  cpmatmcllem  21329  mp2pm2mplem4  21420  cayleyhamilton1  21503  cmpsublem  22010  cmpsub  22011  cmpfii  22020  ptpjcn  22222  isufil2  22519  ufileu  22530  lmmbr  23864  caussi  23903  plyco0  24785  dgrco  24868  emcllem7  25582  isppw2  25695  uvtxnbgrvtx  27178  rusgrnumwwlks  27756  clwwlkf  27829  vdgn1frgrv2  28078  frgrregorufr  28107  grpoidinvlem3  28286  grpoideu  28289  lnconi  29813  fsumiunle  30549  rngurd  30861  tpr2rico  31159  esumiun  31357  0elsiga  31377  sigaclci  31395  dya2icoseg2  31540  derangsn  32421  sat1el2xp  32630  frr3g  33125  fwddifnp1  33630  poimirlem25  34921  poimirlem26  34922  poimirlem30  34926  poimirlem31  34927  poimirlem32  34928  heicant  34931  mblfinlem2  34934  ftc1anc  34979  fdc  35024  bndss  35068  isdrngo2  35240  divrngidl  35310  maxidlmax  35325  cdleme0nex  37430  dihglblem2N  38434  hgmapvs  39031  ismrcd1  39301  nacsfg  39308  isnacs3  39313  nacsfix  39315  mzpcl1  39332  mzpcl2  39333  mzpcong  39575  dnnumch1  39650  aomclem1  39660  aomclem6  39665  lnr2i  39722  hbtlem5  39734  hbt  39736  pwssfi  41313  rexanuz3  41368  choicefi  41469  fsneq  41475  suplesup  41613  xralrple2  41628  infxr  41641  infleinf  41646  xralrple4  41647  xralrple3  41648  xrralrecnnge  41668  supxrunb3  41678  supxrleubrnmpt  41685  unb2ltle  41695  suprleubrnmpt  41702  infxrgelbrnmpt  41736  supminfxr  41746  xrpnf  41768  islpcn  41926  limclner  41938  climd  41959  clim2d  41960  limsupmnflem  42007  limsupre3uzlem  42022  liminflelimsuplem  42062  xlimpnfxnegmnf  42101  xlimxrre  42118  xlimmnfvlem1  42119  xlimmnfv  42121  xlimpnfvlem1  42123  xlimpnfv  42125  climxlim2lem  42132  ioodvbdlimc1lem1  42222  ioodvbdlimc1lem2  42223  ioodvbdlimc2lem  42225  fourierdlem103  42501  fourierdlem104  42502  etransclem48  42574  saluncl  42609  subsaliuncllem  42647  sge0pnffigt  42685  omessle  42787  caragensplit  42789  omeunile  42794  hoidmvlelem2  42885  hoidmvlelem3  42886  hoidmvle  42889  vonvolmbllem  42949  vonvolmbl  42950  pimdecfgtioc  43000  smfpreimalt  43015  smfpreimaltf  43020  smfpreimale  43038  smfpreimagt  43045  smfpreimage  43065  smfmullem4  43076  smfinflem  43098  iccpartrn  43597  iccpartiun  43601  icceuelpart  43603  lidldomn1  44199  ply1mulgsumlem2  44448  lindslinindsimp2lem5  44524  lindslinindsimp2  44525  snlindsntor  44533  nn0sumshdiglemA  44686  nn0sumshdiglemB  44687  nn0sumshdig  44690