Theorem rspcev 2911

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1398   ∈ wcel 2202  ∃wrex 2512

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rex 2517  df-v 2805

This theorem is referenced by:  rspceaimv  2919  rspc2ev  2926  rspc3ev  2928  rspceeqv  2929  reu6i  2998  rspesbca  3118  brralrspcev  4152  nn0suc  4708  elrnmpt1s  4988  elrnrexdm  5794  eldmrexrn  5796  foco2  5904  elabrex  5908  elabrexg  5909  f1elima  5924  fcofo  5935  fliftfun  5947  fliftval  5951  f1oiso2  5978  fo1st  6329  fo2nd  6330  tfr0dm  6531  tfrlemisucaccv  6534  tfrlemi14d  6542  tfrexlem  6543  tfr1onlemsucaccv  6550  tfr1onlemres  6558  tfrcllemsucaccv  6563  tfrcllemres  6571  rdgss  6592  frecabcl  6608  nnaordex  6739  nnawordex  6740  ecelqsg  6800  snfig  7032  nnfi  7102  findcard  7120  fimax2gtrilemstep  7133  unsnfi  7154  eqsupti  7238  supmaxti  7246  supisoex  7251  infminti  7269  finomni  7382  nninfwlpoimlemginf  7418  isnumi  7429  oncardval  7433  archnqq  7680  prarloclemarch2  7682  prcdnql  7747  prcunqu  7748  prarloclemlo  7757  prarloclem5  7763  nqprm  7805  1idprl  7853  1idpru  7854  ltexpri  7876  prplnqu  7883  recexprlemm  7887  recexprlem1ssl  7896  recexprlem1ssu  7897  recexpr  7901  aptiprleml  7902  archpr  7906  cauappcvgprlemm  7908  cauappcvgprlemloc  7915  cauappcvgprlem1  7922  cauappcvgprlem2  7923  cauappcvgpr  7925  caucvgprlemm  7931  caucvgprlemloc  7938  caucvgprlem1  7942  caucvgprlem2  7943  caucvgpr  7945  caucvgprprlemmu  7958  caucvgprprlemopl  7960  caucvgprprlemopu  7962  caucvgprprlemloc  7966  caucvgprprlem1  7972  caucvgprprlem2  7973  caucvgprpr  7975  suplocexprlemmu  7981  suplocexprlemloc  7984  suplocexpr  7988  negexsr  8035  recexgt0sr  8036  caucvgsrlemgt1  8058  caucvgsrlemoffres  8063  suplocsrlem  8071  axrnegex  8142  axprecex  8143  nntopi  8157  axcaucvglemres  8162  axpre-suploclemres  8164  cnegex  8399  recexre  8800  recexap  8875  receuap  8891  rerecapb  9065  sup3exmid  9179  cju  9183  nn2ge  9218  nominpos  9424  zdiv  9612  btwnz  9643  supinfneg  9873  infsupneg  9874  ublbneg  9891  lbzbi  9894  zq  9904  z2ge  10105  iccsupr  10245  zsupcllemstep  10535  infssuzex  10539  suprzubdc  10542  zsupssdc  10544  exbtwnzlemstep  10553  exbtwnzlemex  10555  rebtwn2zlemstep  10558  rebtwn2z  10560  qbtwnre  10562  qbtwnxr  10563  expnbnd  10971  hashunlem  11113  iswrdinn0  11167  shftlem  11439  shftfvalg  11441  shftfval  11444  caucvgre  11604  cvg1nlemres  11608  rexanuz  11611  rexuz3  11613  resqrexlemex  11648  caubnd2  11740  maxabslemval  11831  maxleast  11836  rexanre  11843  rexico  11844  fimaxre2  11850  minmax  11853  xrmaxiflemval  11873  xrmaxaddlem  11883  xrminmax  11888  climconst  11913  climshftlemg  11925  cn1lem  11937  serf0  11975  zsumdc  12008  fsum3  12011  fsum3cvg3  12020  mertenslemi1  12159  ntrivcvgap0  12173  zproddc  12203  fprodseq  12207  fprodntrivap  12208  dvdsval2  12414  dvds0lem  12425  dvds1lem  12426  dvds2lem  12427  odd2np1lem  12496  odd2np1  12497  opeo  12521  omeo  12522  divalglemex  12546  bezoutlemnewy  12630  bezoutlemaz  12637  bezoutlembz  12638  bezoutlemsup  12643  nnwodc  12670  uzwodc  12671  ncoprmgcdne1b  12724  exprmfct  12773  reumodprminv  12889  modprm0  12890  nnnn0modprm0  12891  pythagtriplem19  12918  pcprmpw2  12969  pockthi  12994  infpnlem2  12996  ennnfonelemex  13098  ennnfonelemhom  13099  ennnfonelemrn  13103  ennnfonelemnn0  13106  ennnfonelemim  13108  exmidunben  13110  ctinfomlemom  13111  ctinfom  13112  ctinf  13114  ctiunctlemf  13122  ismgmid2  13526  mgmidsssn0  13530  ismndd  13583  isgrpd2  13667  isgrpd  13669  imasgrp2  13760  mhmmnd  13766  ghmgrp  13768  dvdsrmuld  14174  dvdsr01  14182  rhmdvdsr  14253  lspf  14468  lspval  14469  lssats2  14493  fiinbas  14843  topbas  14861  clsval  14905  neiint  14939  neipsm  14948  opnneissb  14949  opnssneib  14950  innei  14957  restbasg  14962  lmconst  15010  iscnp4  15012  cncnpi  15022  cnconst2  15027  cnptoprest  15033  cnpdis  15036  neitx  15062  txcnp  15065  blssps  15221  blss  15222  blssexps  15223  blssex  15224  ssblex  15225  blin2  15226  neibl  15285  metss2  15292  bdmopn  15298  metrest  15300  metcnp3  15305  tgioo  15348  tgqioo  15349  addcncntoplem  15355  cnopnap  15405  dedekindeulemuub  15411  suplociccreex  15418  dedekindicclemuub  15420  ivthinclemlm  15428  ivthinclemum  15429  ivthinclemlopn  15430  ivthinclemuopn  15432  ivthreinc  15439  elply2  15529  reeff1oleme  15566  sin0pilem2  15576  sgmnncl  15785  dvdsppwf1o  15786  perfect  15798  bj-nn0suc0  16649  bj-inf2vnlem1  16669  3dom  16691  nninfsellemeq  16723  nninfomnilem  16727  qdencn  16738  trirec0  16759  qdiff  16764