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 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1402   ∈ wcel 2209  ∃wrex 2529

This proof depends on 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 proof 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 used by:  rspcedvdw  2936  rspceaimv  2938  rspc2ev  2945  rspc3ev  2947  rspceeqv  2948  reu6i  3017  rspesbca  3137  brralrspcev  4189  nn0suc  4751  elrnmpt1s  5032  elrnrexdm  5847  eldmrexrn  5849  foco2  5959  elabrex  5963  elabrexg  5964  f1elima  5979  fcofo  5990  fliftfun  6002  fliftval  6006  f1oiso2  6033  fo1st  6391  fo2nd  6392  tfr0dm  6593  tfrlemisucaccv  6596  tfrlemi14d  6604  tfrexlem  6605  tfr1onlemsucaccv  6612  tfr1onlemres  6620  tfrcllemsucaccv  6625  tfrcllemres  6633  rdgss  6654  frecabcl  6670  nnaordex  6801  nnawordex  6802  ecelqsg  6862  snfig  7103  nnfi  7174  findcard  7192  fimax2gtrilemstep  7205  unsnfi  7226  eqsupti  7336  supmaxti  7344  supisoex  7349  infminti  7367  finomni  7480  nninfwlpoimlemginf  7516  isnumi  7527  oncardval  7531  archnqq  7784  prarloclemarch2  7786  prcdnql  7851  prcunqu  7852  prarloclemlo  7861  prarloclem5  7867  nqprm  7909  1idprl  7957  1idpru  7958  ltexpri  7980  prplnqu  7987  recexprlemm  7991  recexprlem1ssl  8000  recexprlem1ssu  8001  recexpr  8005  aptiprleml  8006  archpr  8010  cauappcvgprlemm  8012  cauappcvgprlemloc  8019  cauappcvgprlem1  8026  cauappcvgprlem2  8027  cauappcvgpr  8029  caucvgprlemm  8035  caucvgprlemloc  8042  caucvgprlem1  8046  caucvgprlem2  8047  caucvgpr  8049  caucvgprprlemmu  8062  caucvgprprlemopl  8064  caucvgprprlemopu  8066  caucvgprprlemloc  8070  caucvgprprlem1  8076  caucvgprprlem2  8077  caucvgprpr  8079  suplocexprlemmu  8085  suplocexprlemloc  8088  suplocexpr  8092  negexsr  8139  recexgt0sr  8140  caucvgsrlemgt1  8162  caucvgsrlemoffres  8167  suplocsrlem  8175  axrnegex  8246  axprecex  8247  nntopi  8261  axcaucvglemres  8266  axpre-suploclemres  8268  cnegex  8505  recexre  8908  recexap  8983  receuap  9001  rerecapb  9175  sup3exmid  9289  cju  9293  nn2ge  9339  nominpos  9547  zdiv  9738  btwnz  9769  supinfneg  10004  infsupneg  10005  ublbneg  10022  lbzbi  10025  zq  10035  z2ge  10238  iccsupr  10378  zsupcllemstep  10672  infssuzex  10676  suprzubdc  10681  zsupssdc  10683  exbtwnzlemstep  10692  exbtwnzlemex  10694  rebtwn2zlemstep  10697  rebtwn2z  10699  qbtwnre  10701  qbtwnxr  10702  expnbnd  11114  hashunlem  11258  iswrdinn0  11323  shftlem  11595  shftfvalg  11597  shftfval  11600  caucvgre  11761  cvg1nlemres  11765  rexanuz  11768  rexuz3  11770  resqrexlemex  11805  caubnd2  11898  maxabslemval  11989  maxleast  11994  rexanre  12001  rexico  12002  fimaxre2  12008  minmax  12011  xrmaxiflemval  12032  xrmaxaddlem  12042  xrminmax  12047  climconst  12072  climshftlemg  12084  cn1lem  12096  serf0  12134  zsumdc  12167  fsum3  12170  fsum3cvg3  12179  mertenslemi1  12318  ntrivcvgap0  12332  zproddc  12362  fprodseq  12366  fprodntrivap  12367  dvdsval2  12573  dvds0lem  12584  dvds1lem  12585  dvds2lem  12586  odd2np1lem  12655  odd2np1  12656  opeo  12680  omeo  12681  divalglemex  12705  bezoutlemnewy  12789  bezoutlemaz  12796  bezoutlembz  12797  bezoutlemsup  12802  nnwodc  12829  uzwodc  12830  ncoprmgcdne1b  12883  exprmfct  12933  reumodprminv  13052  modprm0  13053  nnnn0modprm0  13054  pythagtriplem19  13081  pcprmpw2  13132  pockthi  13157  infpnlem2  13159  ballotfilem4  13290  ballotfilemic  13299  ennnfonelemex  13354  ennnfonelemhom  13355  ennnfonelemrn  13359  ennnfonelemnn0  13362  ennnfonelemim  13364  exmidunben  13366  ctinfomlemom  13367  ctinfom  13368  ctinf  13370  ctiunctlemf  13378  ismgmid2  13749  mgmidsssn0  13753  ismndd  13799  isgrpd2  13875  isgrpd  13877  imasgrp2  13962  mhmmnd  13968  ghmgrp  13970  dvdsrmuld  14452  dvdsr01  14460  rhmdvdsr  14531  lspf  14775  lspval  14776  lssats2  14800  aspval  15064  fiinbas  15199  topbas  15217  clsval  15261  neiint  15295  neipsm  15304  opnneissb  15305  opnssneib  15306  innei  15313  restbasg  15318  lmconst  15366  iscnp4  15368  cncnpi  15378  cnconst2  15383  cnptoprest  15389  cnpdis  15392  neitx  15418  txcnp  15421  blssps  15577  blss  15578  blssexps  15579  blssex  15580  ssblex  15581  blin2  15582  neibl  15641  metss2  15648  bdmopn  15654  metrest  15656  metcnp3  15661  tgioo  15704  tgqioo  15705  addcncntoplem  15711  cnopnap  15761  dedekindeulemuub  15767  suplociccreex  15774  dedekindicclemuub  15776  ivthinclemlm  15784  ivthinclemum  15785  ivthinclemlopn  15786  ivthinclemuopn  15788  ivthreinc  15795  elply2  15885  reeff1oleme  15922  sin0pilem2  15933  sgmnncl  16169  dvdsppwf1o  16184  perfect  16199  bpos1lem  16207  bj-nn0suc0  17074  bj-inf2vnlem1  17094  3dom  17116  nninfsellemeq  17155  nninfomnilem  17159  qdencn  17170  trirec0  17191  qdiff  17196