Theorem rspcev 2929

Description: Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.)

Hypothesis

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

Assertion

Ref	Expression
rspcev	⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)

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

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rspcev

Step	Hyp	Ref	Expression
1		nfv 1581	. 2 ⊢ Ⅎ𝑥𝜓
2		rspcv.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	1, 2	rspce 2924	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1402   ∈ wcel 2209  ∃wrex 2529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-v 2823

This theorem is referenced by:  rspcedvdw  2936  rspceaimv  2938  rspc2ev  2945  rspc3ev  2947  rspceeqv  2948  reu6i  3017  rspesbca  3137  brralrspcev  4184  nn0suc  4746  elrnmpt1s  5027  elrnrexdm  5838  eldmrexrn  5840  foco2  5949  elabrex  5953  elabrexg  5954  f1elima  5969  fcofo  5980  fliftfun  5992  fliftval  5996  f1oiso2  6023  fo1st  6381  fo2nd  6382  tfr0dm  6583  tfrlemisucaccv  6586  tfrlemi14d  6594  tfrexlem  6595  tfr1onlemsucaccv  6602  tfr1onlemres  6610  tfrcllemsucaccv  6615  tfrcllemres  6623  rdgss  6644  frecabcl  6660  nnaordex  6791  nnawordex  6792  ecelqsg  6852  snfig  7093  nnfi  7164  findcard  7182  fimax2gtrilemstep  7195  unsnfi  7216  eqsupti  7326  supmaxti  7334  supisoex  7339  infminti  7357  finomni  7470  nninfwlpoimlemginf  7506  isnumi  7517  oncardval  7521  archnqq  7774  prarloclemarch2  7776  prcdnql  7841  prcunqu  7842  prarloclemlo  7851  prarloclem5  7857  nqprm  7899  1idprl  7947  1idpru  7948  ltexpri  7970  prplnqu  7977  recexprlemm  7981  recexprlem1ssl  7990  recexprlem1ssu  7991  recexpr  7995  aptiprleml  7996  archpr  8000  cauappcvgprlemm  8002  cauappcvgprlemloc  8009  cauappcvgprlem1  8016  cauappcvgprlem2  8017  cauappcvgpr  8019  caucvgprlemm  8025  caucvgprlemloc  8032  caucvgprlem1  8036  caucvgprlem2  8037  caucvgpr  8039  caucvgprprlemmu  8052  caucvgprprlemopl  8054  caucvgprprlemopu  8056  caucvgprprlemloc  8060  caucvgprprlem1  8066  caucvgprprlem2  8067  caucvgprpr  8069  suplocexprlemmu  8075  suplocexprlemloc  8078  suplocexpr  8082  negexsr  8129  recexgt0sr  8130  caucvgsrlemgt1  8152  caucvgsrlemoffres  8157  suplocsrlem  8165  axrnegex  8236  axprecex  8237  nntopi  8251  axcaucvglemres  8256  axpre-suploclemres  8258  cnegex  8494  recexre  8896  recexap  8971  receuap  8989  rerecapb  9163  sup3exmid  9277  cju  9281  nn2ge  9316  nominpos  9522  zdiv  9713  btwnz  9744  supinfneg  9974  infsupneg  9975  ublbneg  9992  lbzbi  9995  zq  10005  z2ge  10207  iccsupr  10347  zsupcllemstep  10640  infssuzex  10644  suprzubdc  10649  zsupssdc  10651  exbtwnzlemstep  10660  exbtwnzlemex  10662  rebtwn2zlemstep  10665  rebtwn2z  10667  qbtwnre  10669  qbtwnxr  10670  expnbnd  11079  hashunlem  11222  iswrdinn0  11287  shftlem  11559  shftfvalg  11561  shftfval  11564  caucvgre  11725  cvg1nlemres  11729  rexanuz  11732  rexuz3  11734  resqrexlemex  11769  caubnd2  11861  maxabslemval  11952  maxleast  11957  rexanre  11964  rexico  11965  fimaxre2  11971  minmax  11974  xrmaxiflemval  11994  xrmaxaddlem  12004  xrminmax  12009  climconst  12034  climshftlemg  12046  cn1lem  12058  serf0  12096  zsumdc  12129  fsum3  12132  fsum3cvg3  12141  mertenslemi1  12280  ntrivcvgap0  12294  zproddc  12324  fprodseq  12328  fprodntrivap  12329  dvdsval2  12535  dvds0lem  12546  dvds1lem  12547  dvds2lem  12548  odd2np1lem  12617  odd2np1  12618  opeo  12642  omeo  12643  divalglemex  12667  bezoutlemnewy  12751  bezoutlemaz  12758  bezoutlembz  12759  bezoutlemsup  12764  nnwodc  12791  uzwodc  12792  ncoprmgcdne1b  12845  exprmfct  12894  reumodprminv  13010  modprm0  13011  nnnn0modprm0  13012  pythagtriplem19  13039  pcprmpw2  13090  pockthi  13115  infpnlem2  13117  ballotfilem4  13219  ballotfilemic  13228  ennnfonelemex  13283  ennnfonelemhom  13284  ennnfonelemrn  13288  ennnfonelemnn0  13291  ennnfonelemim  13293  exmidunben  13295  ctinfomlemom  13296  ctinfom  13297  ctinf  13299  ctiunctlemf  13307  ismgmid2  13677  mgmidsssn0  13681  ismndd  13727  isgrpd2  13803  isgrpd  13805  imasgrp2  13890  mhmmnd  13896  ghmgrp  13898  dvdsrmuld  14376  dvdsr01  14384  rhmdvdsr  14455  lspf  14698  lspval  14699  lssats2  14723  fiinbas  15073  topbas  15091  clsval  15135  neiint  15169  neipsm  15178  opnneissb  15179  opnssneib  15180  innei  15187  restbasg  15192  lmconst  15240  iscnp4  15242  cncnpi  15252  cnconst2  15257  cnptoprest  15263  cnpdis  15266  neitx  15292  txcnp  15295  blssps  15451  blss  15452  blssexps  15453  blssex  15454  ssblex  15455  blin2  15456  neibl  15515  metss2  15522  bdmopn  15528  metrest  15530  metcnp3  15535  tgioo  15578  tgqioo  15579  addcncntoplem  15585  cnopnap  15635  dedekindeulemuub  15641  suplociccreex  15648  dedekindicclemuub  15650  ivthinclemlm  15658  ivthinclemum  15659  ivthinclemlopn  15660  ivthinclemuopn  15662  ivthreinc  15669  elply2  15759  reeff1oleme  15796  sin0pilem2  15806  sgmnncl  16016  dvdsppwf1o  16017  perfect  16029  bj-nn0suc0  16890  bj-inf2vnlem1  16910  3dom  16932  nninfsellemeq  16962  nninfomnilem  16966  qdencn  16977  trirec0  16998  qdiff  17003