Theorem rspcev 2843

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1353   ∈ wcel 2148  ∃wrex 2456

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2741

This theorem is referenced by:  rspceaimv  2851  rspc2ev  2858  rspc3ev  2860  rspceeqv  2861  reu6i  2930  rspesbca  3049  brralrspcev  4063  nn0suc  4605  elrnmpt1s  4879  elrnrexdm  5657  eldmrexrn  5659  foco2  5756  elabrex  5760  elabrexg  5761  f1elima  5776  fcofo  5787  fliftfun  5799  fliftval  5803  f1oiso2  5830  fo1st  6160  fo2nd  6161  tfr0dm  6325  tfrlemisucaccv  6328  tfrlemi14d  6336  tfrexlem  6337  tfr1onlemsucaccv  6344  tfr1onlemres  6352  tfrcllemsucaccv  6357  tfrcllemres  6365  rdgss  6386  frecabcl  6402  nnaordex  6531  nnawordex  6532  ecelqsg  6590  snfig  6816  nnfi  6874  findcard  6890  fimax2gtrilemstep  6902  unsnfi  6920  eqsupti  6997  supmaxti  7005  supisoex  7010  infminti  7028  finomni  7140  nninfwlpoimlemginf  7176  isnumi  7183  oncardval  7187  archnqq  7418  prarloclemarch2  7420  prcdnql  7485  prcunqu  7486  prarloclemlo  7495  prarloclem5  7501  nqprm  7543  1idprl  7591  1idpru  7592  ltexpri  7614  prplnqu  7621  recexprlemm  7625  recexprlem1ssl  7634  recexprlem1ssu  7635  recexpr  7639  aptiprleml  7640  archpr  7644  cauappcvgprlemm  7646  cauappcvgprlemloc  7653  cauappcvgprlem1  7660  cauappcvgprlem2  7661  cauappcvgpr  7663  caucvgprlemm  7669  caucvgprlemloc  7676  caucvgprlem1  7680  caucvgprlem2  7681  caucvgpr  7683  caucvgprprlemmu  7696  caucvgprprlemopl  7698  caucvgprprlemopu  7700  caucvgprprlemloc  7704  caucvgprprlem1  7710  caucvgprprlem2  7711  caucvgprpr  7713  suplocexprlemmu  7719  suplocexprlemloc  7722  suplocexpr  7726  negexsr  7773  recexgt0sr  7774  caucvgsrlemgt1  7796  caucvgsrlemoffres  7801  suplocsrlem  7809  axrnegex  7880  axprecex  7881  nntopi  7895  axcaucvglemres  7900  axpre-suploclemres  7902  cnegex  8137  recexre  8537  recexap  8612  receuap  8628  rerecapb  8802  sup3exmid  8916  cju  8920  nn2ge  8954  nominpos  9158  zdiv  9343  btwnz  9374  supinfneg  9597  infsupneg  9598  ublbneg  9615  lbzbi  9618  zq  9628  z2ge  9828  iccsupr  9968  exbtwnzlemstep  10250  exbtwnzlemex  10252  rebtwn2zlemstep  10255  rebtwn2z  10257  qbtwnre  10259  qbtwnxr  10260  expnbnd  10646  hashunlem  10786  shftlem  10827  shftfvalg  10829  shftfval  10832  caucvgre  10992  cvg1nlemres  10996  rexanuz  10999  rexuz3  11001  resqrexlemex  11036  caubnd2  11128  maxabslemval  11219  maxleast  11224  rexanre  11231  rexico  11232  fimaxre2  11237  minmax  11240  xrmaxiflemval  11260  xrmaxaddlem  11270  xrminmax  11275  climconst  11300  climshftlemg  11312  cn1lem  11324  serf0  11362  zsumdc  11394  fsum3  11397  fsum3cvg3  11406  mertenslemi1  11545  ntrivcvgap0  11559  zproddc  11589  fprodseq  11593  fprodntrivap  11594  dvdsval2  11799  dvds0lem  11810  dvds1lem  11811  dvds2lem  11812  odd2np1lem  11879  odd2np1  11880  opeo  11904  omeo  11905  divalglemex  11929  zsupcllemstep  11948  infssuzex  11952  suprzubdc  11955  zsupssdc  11957  bezoutlemnewy  11999  bezoutlemaz  12006  bezoutlembz  12007  bezoutlemsup  12012  nnwodc  12039  uzwodc  12040  ncoprmgcdne1b  12091  exprmfct  12140  reumodprminv  12255  modprm0  12256  nnnn0modprm0  12257  pythagtriplem19  12284  pcprmpw2  12334  pockthi  12358  infpnlem2  12360  ennnfonelemex  12417  ennnfonelemhom  12418  ennnfonelemrn  12422  ennnfonelemnn0  12425  ennnfonelemim  12427  exmidunben  12429  ctinfomlemom  12430  ctinfom  12431  ctinf  12433  ctiunctlemf  12441  ismgmid2  12804  mgmidsssn0  12808  ismndd  12843  isgrpd2  12902  isgrpd  12904  mhmmnd  12985  ghmgrp  12987  dvdsrmuld  13270  dvdsr01  13278  fiinbas  13588  topbas  13606  clsval  13650  neiint  13684  neipsm  13693  opnneissb  13694  opnssneib  13695  innei  13702  restbasg  13707  lmconst  13755  iscnp4  13757  cncnpi  13767  cnconst2  13772  cnptoprest  13778  cnpdis  13781  neitx  13807  txcnp  13810  blssps  13966  blss  13967  blssexps  13968  blssex  13969  ssblex  13970  blin2  13971  neibl  14030  metss2  14037  bdmopn  14043  metrest  14045  metcnp3  14050  tgioo  14085  tgqioo  14086  addcncntoplem  14090  cnopnap  14133  dedekindeulemuub  14134  suplociccreex  14141  dedekindicclemuub  14143  ivthinclemlm  14151  ivthinclemum  14152  ivthinclemlopn  14153  ivthinclemuopn  14155  reeff1oleme  14232  sin0pilem2  14242  bj-nn0suc0  14741  bj-inf2vnlem1  14761  nninfsellemeq  14802  nninfomnilem  14806  qdencn  14814  trirec0  14831