Theorem rspcev 2784

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

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1331   ∈ wcel 1480  ∃wrex 2415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-rex 2420  df-v 2683

This theorem is referenced by:  rspceaimv  2792  rspc2ev  2799  rspc3ev  2801  rspceeqv  2802  reu6i  2870  rspesbca  2988  brralrspcev  3981  nn0suc  4513  elrnmpt1s  4784  elrnrexdm  5552  eldmrexrn  5554  foco2  5648  elabrex  5652  f1elima  5667  fcofo  5678  fliftfun  5690  fliftval  5694  f1oiso2  5721  fo1st  6048  fo2nd  6049  tfr0dm  6212  tfrlemisucaccv  6215  tfrlemi14d  6223  tfrexlem  6224  tfr1onlemsucaccv  6231  tfr1onlemres  6239  tfrcllemsucaccv  6244  tfrcllemres  6252  rdgss  6273  frecabcl  6289  nnaordex  6416  nnawordex  6417  ecelqsg  6475  snfig  6701  nnfi  6759  findcard  6775  fimax2gtrilemstep  6787  unsnfi  6800  eqsupti  6876  supmaxti  6884  supisoex  6889  infminti  6907  finomni  7005  isnumi  7031  oncardval  7035  archnqq  7218  prarloclemarch2  7220  prcdnql  7285  prcunqu  7286  prarloclemlo  7295  prarloclem5  7301  nqprm  7343  1idprl  7391  1idpru  7392  ltexpri  7414  prplnqu  7421  recexprlemm  7425  recexprlem1ssl  7434  recexprlem1ssu  7435  recexpr  7439  aptiprleml  7440  archpr  7444  cauappcvgprlemm  7446  cauappcvgprlemloc  7453  cauappcvgprlem1  7460  cauappcvgprlem2  7461  cauappcvgpr  7463  caucvgprlemm  7469  caucvgprlemloc  7476  caucvgprlem1  7480  caucvgprlem2  7481  caucvgpr  7483  caucvgprprlemmu  7496  caucvgprprlemopl  7498  caucvgprprlemopu  7500  caucvgprprlemloc  7504  caucvgprprlem1  7510  caucvgprprlem2  7511  caucvgprpr  7513  suplocexprlemmu  7519  suplocexprlemloc  7522  suplocexpr  7526  negexsr  7573  recexgt0sr  7574  caucvgsrlemgt1  7596  caucvgsrlemoffres  7601  suplocsrlem  7609  axrnegex  7680  axprecex  7681  nntopi  7695  axcaucvglemres  7700  axpre-suploclemres  7702  cnegex  7933  recexre  8333  recexap  8407  receuap  8423  sup3exmid  8708  cju  8712  nn2ge  8746  nominpos  8950  zdiv  9132  btwnz  9163  supinfneg  9383  infsupneg  9384  ublbneg  9398  lbzbi  9401  zq  9411  z2ge  9602  iccsupr  9742  exbtwnzlemstep  10018  exbtwnzlemex  10020  rebtwn2zlemstep  10023  rebtwn2z  10025  qbtwnre  10027  qbtwnxr  10028  expnbnd  10408  hashunlem  10543  shftlem  10581  shftfvalg  10583  shftfval  10586  caucvgre  10746  cvg1nlemres  10750  rexanuz  10753  rexuz3  10755  resqrexlemex  10790  caubnd2  10882  maxabslemval  10973  maxleast  10978  rexanre  10985  rexico  10986  fimaxre2  10991  minmax  10994  xrmaxiflemval  11012  xrmaxaddlem  11022  xrminmax  11027  climconst  11052  climshftlemg  11064  cn1lem  11076  serf0  11114  zsumdc  11146  fsum3  11149  fsum3cvg3  11158  mertenslemi1  11297  ntrivcvgap0  11311  dvdsval2  11485  dvds0lem  11492  dvds1lem  11493  dvds2lem  11494  odd2np1lem  11558  odd2np1  11559  opeo  11583  omeo  11584  divalglemex  11608  zsupcllemstep  11627  infssuzex  11631  bezoutlemnewy  11673  bezoutlemaz  11680  bezoutlembz  11681  bezoutlemsup  11686  ncoprmgcdne1b  11759  exprmfct  11807  ennnfonelemex  11916  ennnfonelemhom  11917  ennnfonelemrn  11921  ennnfonelemnn0  11924  ennnfonelemim  11926  exmidunben  11928  ctinfomlemom  11929  ctinfom  11930  ctinf  11932  ctiunctlemf  11940  fiinbas  12205  topbas  12225  clsval  12269  neiint  12303  neipsm  12312  opnneissb  12313  opnssneib  12314  innei  12321  restbasg  12326  lmconst  12374  iscnp4  12376  cncnpi  12386  cnconst2  12391  cnptoprest  12397  cnpdis  12400  neitx  12426  txcnp  12429  blssps  12585  blss  12586  blssexps  12587  blssex  12588  ssblex  12589  blin2  12590  neibl  12649  metss2  12656  bdmopn  12662  metrest  12664  metcnp3  12669  tgioo  12704  tgqioo  12705  addcncntoplem  12709  cnopnap  12752  dedekindeulemuub  12753  suplociccreex  12760  dedekindicclemuub  12762  ivthinclemlm  12770  ivthinclemum  12771  ivthinclemlopn  12772  ivthinclemuopn  12774  sin0pilem2  12852  bj-nn0suc0  13137  bj-inf2vnlem1  13157  nninfsellemeq  13199  nninfomnilem  13203  qdencn  13211