Theorem rspcev 2907

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 1574	. 2 ⊢ Ⅎ𝑥𝜓
2		rspcv.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	1, 2	rspce 2902	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1395   ∈ wcel 2200  ∃wrex 2509

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2801

This theorem is referenced by:  rspceaimv  2915  rspc2ev  2922  rspc3ev  2924  rspceeqv  2925  reu6i  2994  rspesbca  3114  brralrspcev  4142  nn0suc  4696  elrnmpt1s  4974  elrnrexdm  5776  eldmrexrn  5778  foco2  5883  elabrex  5887  elabrexg  5888  f1elima  5903  fcofo  5914  fliftfun  5926  fliftval  5930  f1oiso2  5957  fo1st  6309  fo2nd  6310  tfr0dm  6474  tfrlemisucaccv  6477  tfrlemi14d  6485  tfrexlem  6486  tfr1onlemsucaccv  6493  tfr1onlemres  6501  tfrcllemsucaccv  6506  tfrcllemres  6514  rdgss  6535  frecabcl  6551  nnaordex  6682  nnawordex  6683  ecelqsg  6743  snfig  6975  nnfi  7042  findcard  7058  fimax2gtrilemstep  7071  unsnfi  7092  eqsupti  7174  supmaxti  7182  supisoex  7187  infminti  7205  finomni  7318  nninfwlpoimlemginf  7354  isnumi  7365  oncardval  7369  archnqq  7615  prarloclemarch2  7617  prcdnql  7682  prcunqu  7683  prarloclemlo  7692  prarloclem5  7698  nqprm  7740  1idprl  7788  1idpru  7789  ltexpri  7811  prplnqu  7818  recexprlemm  7822  recexprlem1ssl  7831  recexprlem1ssu  7832  recexpr  7836  aptiprleml  7837  archpr  7841  cauappcvgprlemm  7843  cauappcvgprlemloc  7850  cauappcvgprlem1  7857  cauappcvgprlem2  7858  cauappcvgpr  7860  caucvgprlemm  7866  caucvgprlemloc  7873  caucvgprlem1  7877  caucvgprlem2  7878  caucvgpr  7880  caucvgprprlemmu  7893  caucvgprprlemopl  7895  caucvgprprlemopu  7897  caucvgprprlemloc  7901  caucvgprprlem1  7907  caucvgprprlem2  7908  caucvgprpr  7910  suplocexprlemmu  7916  suplocexprlemloc  7919  suplocexpr  7923  negexsr  7970  recexgt0sr  7971  caucvgsrlemgt1  7993  caucvgsrlemoffres  7998  suplocsrlem  8006  axrnegex  8077  axprecex  8078  nntopi  8092  axcaucvglemres  8097  axpre-suploclemres  8099  cnegex  8335  recexre  8736  recexap  8811  receuap  8827  rerecapb  9001  sup3exmid  9115  cju  9119  nn2ge  9154  nominpos  9360  zdiv  9546  btwnz  9577  supinfneg  9802  infsupneg  9803  ublbneg  9820  lbzbi  9823  zq  9833  z2ge  10034  iccsupr  10174  zsupcllemstep  10461  infssuzex  10465  suprzubdc  10468  zsupssdc  10470  exbtwnzlemstep  10479  exbtwnzlemex  10481  rebtwn2zlemstep  10484  rebtwn2z  10486  qbtwnre  10488  qbtwnxr  10489  expnbnd  10897  hashunlem  11038  iswrdinn0  11089  shftlem  11342  shftfvalg  11344  shftfval  11347  caucvgre  11507  cvg1nlemres  11511  rexanuz  11514  rexuz3  11516  resqrexlemex  11551  caubnd2  11643  maxabslemval  11734  maxleast  11739  rexanre  11746  rexico  11747  fimaxre2  11753  minmax  11756  xrmaxiflemval  11776  xrmaxaddlem  11786  xrminmax  11791  climconst  11816  climshftlemg  11828  cn1lem  11840  serf0  11878  zsumdc  11910  fsum3  11913  fsum3cvg3  11922  mertenslemi1  12061  ntrivcvgap0  12075  zproddc  12105  fprodseq  12109  fprodntrivap  12110  dvdsval2  12316  dvds0lem  12327  dvds1lem  12328  dvds2lem  12329  odd2np1lem  12398  odd2np1  12399  opeo  12423  omeo  12424  divalglemex  12448  bezoutlemnewy  12532  bezoutlemaz  12539  bezoutlembz  12540  bezoutlemsup  12545  nnwodc  12572  uzwodc  12573  ncoprmgcdne1b  12626  exprmfct  12675  reumodprminv  12791  modprm0  12792  nnnn0modprm0  12793  pythagtriplem19  12820  pcprmpw2  12871  pockthi  12896  infpnlem2  12898  ennnfonelemex  13000  ennnfonelemhom  13001  ennnfonelemrn  13005  ennnfonelemnn0  13008  ennnfonelemim  13010  exmidunben  13012  ctinfomlemom  13013  ctinfom  13014  ctinf  13016  ctiunctlemf  13024  ismgmid2  13428  mgmidsssn0  13432  ismndd  13485  isgrpd2  13569  isgrpd  13571  imasgrp2  13662  mhmmnd  13668  ghmgrp  13670  dvdsrmuld  14075  dvdsr01  14083  rhmdvdsr  14154  lspf  14368  lspval  14369  lssats2  14393  fiinbas  14738  topbas  14756  clsval  14800  neiint  14834  neipsm  14843  opnneissb  14844  opnssneib  14845  innei  14852  restbasg  14857  lmconst  14905  iscnp4  14907  cncnpi  14917  cnconst2  14922  cnptoprest  14928  cnpdis  14931  neitx  14957  txcnp  14960  blssps  15116  blss  15117  blssexps  15118  blssex  15119  ssblex  15120  blin2  15121  neibl  15180  metss2  15187  bdmopn  15193  metrest  15195  metcnp3  15200  tgioo  15243  tgqioo  15244  addcncntoplem  15250  cnopnap  15300  dedekindeulemuub  15306  suplociccreex  15313  dedekindicclemuub  15315  ivthinclemlm  15323  ivthinclemum  15324  ivthinclemlopn  15325  ivthinclemuopn  15327  ivthreinc  15334  elply2  15424  reeff1oleme  15461  sin0pilem2  15471  sgmnncl  15677  dvdsppwf1o  15678  perfect  15690  bj-nn0suc0  16368  bj-inf2vnlem1  16388  3dom  16411  nninfsellemeq  16440  nninfomnilem  16444  qdencn  16455  trirec0  16472