Theorem rspcev 2910

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

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

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-v 2804

This theorem is referenced by:  rspceaimv  2918  rspc2ev  2925  rspc3ev  2927  rspceeqv  2928  reu6i  2997  rspesbca  3117  brralrspcev  4147  nn0suc  4702  elrnmpt1s  4982  elrnrexdm  5786  eldmrexrn  5788  foco2  5894  elabrex  5898  elabrexg  5899  f1elima  5914  fcofo  5925  fliftfun  5937  fliftval  5941  f1oiso2  5968  fo1st  6320  fo2nd  6321  tfr0dm  6488  tfrlemisucaccv  6491  tfrlemi14d  6499  tfrexlem  6500  tfr1onlemsucaccv  6507  tfr1onlemres  6515  tfrcllemsucaccv  6520  tfrcllemres  6528  rdgss  6549  frecabcl  6565  nnaordex  6696  nnawordex  6697  ecelqsg  6757  snfig  6989  nnfi  7059  findcard  7077  fimax2gtrilemstep  7090  unsnfi  7111  eqsupti  7195  supmaxti  7203  supisoex  7208  infminti  7226  finomni  7339  nninfwlpoimlemginf  7375  isnumi  7386  oncardval  7390  archnqq  7637  prarloclemarch2  7639  prcdnql  7704  prcunqu  7705  prarloclemlo  7714  prarloclem5  7720  nqprm  7762  1idprl  7810  1idpru  7811  ltexpri  7833  prplnqu  7840  recexprlemm  7844  recexprlem1ssl  7853  recexprlem1ssu  7854  recexpr  7858  aptiprleml  7859  archpr  7863  cauappcvgprlemm  7865  cauappcvgprlemloc  7872  cauappcvgprlem1  7879  cauappcvgprlem2  7880  cauappcvgpr  7882  caucvgprlemm  7888  caucvgprlemloc  7895  caucvgprlem1  7899  caucvgprlem2  7900  caucvgpr  7902  caucvgprprlemmu  7915  caucvgprprlemopl  7917  caucvgprprlemopu  7919  caucvgprprlemloc  7923  caucvgprprlem1  7929  caucvgprprlem2  7930  caucvgprpr  7932  suplocexprlemmu  7938  suplocexprlemloc  7941  suplocexpr  7945  negexsr  7992  recexgt0sr  7993  caucvgsrlemgt1  8015  caucvgsrlemoffres  8020  suplocsrlem  8028  axrnegex  8099  axprecex  8100  nntopi  8114  axcaucvglemres  8119  axpre-suploclemres  8121  cnegex  8357  recexre  8758  recexap  8833  receuap  8849  rerecapb  9023  sup3exmid  9137  cju  9141  nn2ge  9176  nominpos  9382  zdiv  9568  btwnz  9599  supinfneg  9829  infsupneg  9830  ublbneg  9847  lbzbi  9850  zq  9860  z2ge  10061  iccsupr  10201  zsupcllemstep  10490  infssuzex  10494  suprzubdc  10497  zsupssdc  10499  exbtwnzlemstep  10508  exbtwnzlemex  10510  rebtwn2zlemstep  10513  rebtwn2z  10515  qbtwnre  10517  qbtwnxr  10518  expnbnd  10926  hashunlem  11068  iswrdinn0  11122  shftlem  11394  shftfvalg  11396  shftfval  11399  caucvgre  11559  cvg1nlemres  11563  rexanuz  11566  rexuz3  11568  resqrexlemex  11603  caubnd2  11695  maxabslemval  11786  maxleast  11791  rexanre  11798  rexico  11799  fimaxre2  11805  minmax  11808  xrmaxiflemval  11828  xrmaxaddlem  11838  xrminmax  11843  climconst  11868  climshftlemg  11880  cn1lem  11892  serf0  11930  zsumdc  11963  fsum3  11966  fsum3cvg3  11975  mertenslemi1  12114  ntrivcvgap0  12128  zproddc  12158  fprodseq  12162  fprodntrivap  12163  dvdsval2  12369  dvds0lem  12380  dvds1lem  12381  dvds2lem  12382  odd2np1lem  12451  odd2np1  12452  opeo  12476  omeo  12477  divalglemex  12501  bezoutlemnewy  12585  bezoutlemaz  12592  bezoutlembz  12593  bezoutlemsup  12598  nnwodc  12625  uzwodc  12626  ncoprmgcdne1b  12679  exprmfct  12728  reumodprminv  12844  modprm0  12845  nnnn0modprm0  12846  pythagtriplem19  12873  pcprmpw2  12924  pockthi  12949  infpnlem2  12951  ennnfonelemex  13053  ennnfonelemhom  13054  ennnfonelemrn  13058  ennnfonelemnn0  13061  ennnfonelemim  13063  exmidunben  13065  ctinfomlemom  13066  ctinfom  13067  ctinf  13069  ctiunctlemf  13077  ismgmid2  13481  mgmidsssn0  13485  ismndd  13538  isgrpd2  13622  isgrpd  13624  imasgrp2  13715  mhmmnd  13721  ghmgrp  13723  dvdsrmuld  14129  dvdsr01  14137  rhmdvdsr  14208  lspf  14422  lspval  14423  lssats2  14447  fiinbas  14792  topbas  14810  clsval  14854  neiint  14888  neipsm  14897  opnneissb  14898  opnssneib  14899  innei  14906  restbasg  14911  lmconst  14959  iscnp4  14961  cncnpi  14971  cnconst2  14976  cnptoprest  14982  cnpdis  14985  neitx  15011  txcnp  15014  blssps  15170  blss  15171  blssexps  15172  blssex  15173  ssblex  15174  blin2  15175  neibl  15234  metss2  15241  bdmopn  15247  metrest  15249  metcnp3  15254  tgioo  15297  tgqioo  15298  addcncntoplem  15304  cnopnap  15354  dedekindeulemuub  15360  suplociccreex  15367  dedekindicclemuub  15369  ivthinclemlm  15377  ivthinclemum  15378  ivthinclemlopn  15379  ivthinclemuopn  15381  ivthreinc  15388  elply2  15478  reeff1oleme  15515  sin0pilem2  15525  sgmnncl  15731  dvdsppwf1o  15732  perfect  15744  bj-nn0suc0  16596  bj-inf2vnlem1  16616  3dom  16638  nninfsellemeq  16667  nninfomnilem  16671  qdencn  16682  trirec0  16699  qdiff  16704