Theorem rspcev 2868

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1364   ∈ wcel 2167  ∃wrex 2476

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-v 2765

This theorem is referenced by:  rspceaimv  2876  rspc2ev  2883  rspc3ev  2885  rspceeqv  2886  reu6i  2955  rspesbca  3074  brralrspcev  4092  nn0suc  4641  elrnmpt1s  4917  elrnrexdm  5704  eldmrexrn  5706  foco2  5803  elabrex  5807  elabrexg  5808  f1elima  5823  fcofo  5834  fliftfun  5846  fliftval  5850  f1oiso2  5877  fo1st  6224  fo2nd  6225  tfr0dm  6389  tfrlemisucaccv  6392  tfrlemi14d  6400  tfrexlem  6401  tfr1onlemsucaccv  6408  tfr1onlemres  6416  tfrcllemsucaccv  6421  tfrcllemres  6429  rdgss  6450  frecabcl  6466  nnaordex  6595  nnawordex  6596  ecelqsg  6656  snfig  6882  nnfi  6942  findcard  6958  fimax2gtrilemstep  6970  unsnfi  6989  eqsupti  7071  supmaxti  7079  supisoex  7084  infminti  7102  finomni  7215  nninfwlpoimlemginf  7251  isnumi  7262  oncardval  7266  archnqq  7503  prarloclemarch2  7505  prcdnql  7570  prcunqu  7571  prarloclemlo  7580  prarloclem5  7586  nqprm  7628  1idprl  7676  1idpru  7677  ltexpri  7699  prplnqu  7706  recexprlemm  7710  recexprlem1ssl  7719  recexprlem1ssu  7720  recexpr  7724  aptiprleml  7725  archpr  7729  cauappcvgprlemm  7731  cauappcvgprlemloc  7738  cauappcvgprlem1  7745  cauappcvgprlem2  7746  cauappcvgpr  7748  caucvgprlemm  7754  caucvgprlemloc  7761  caucvgprlem1  7765  caucvgprlem2  7766  caucvgpr  7768  caucvgprprlemmu  7781  caucvgprprlemopl  7783  caucvgprprlemopu  7785  caucvgprprlemloc  7789  caucvgprprlem1  7795  caucvgprprlem2  7796  caucvgprpr  7798  suplocexprlemmu  7804  suplocexprlemloc  7807  suplocexpr  7811  negexsr  7858  recexgt0sr  7859  caucvgsrlemgt1  7881  caucvgsrlemoffres  7886  suplocsrlem  7894  axrnegex  7965  axprecex  7966  nntopi  7980  axcaucvglemres  7985  axpre-suploclemres  7987  cnegex  8223  recexre  8624  recexap  8699  receuap  8715  rerecapb  8889  sup3exmid  9003  cju  9007  nn2ge  9042  nominpos  9248  zdiv  9433  btwnz  9464  supinfneg  9688  infsupneg  9689  ublbneg  9706  lbzbi  9709  zq  9719  z2ge  9920  iccsupr  10060  zsupcllemstep  10338  infssuzex  10342  suprzubdc  10345  zsupssdc  10347  exbtwnzlemstep  10356  exbtwnzlemex  10358  rebtwn2zlemstep  10361  rebtwn2z  10363  qbtwnre  10365  qbtwnxr  10366  expnbnd  10774  hashunlem  10915  iswrdinn0  10959  shftlem  11000  shftfvalg  11002  shftfval  11005  caucvgre  11165  cvg1nlemres  11169  rexanuz  11172  rexuz3  11174  resqrexlemex  11209  caubnd2  11301  maxabslemval  11392  maxleast  11397  rexanre  11404  rexico  11405  fimaxre2  11411  minmax  11414  xrmaxiflemval  11434  xrmaxaddlem  11444  xrminmax  11449  climconst  11474  climshftlemg  11486  cn1lem  11498  serf0  11536  zsumdc  11568  fsum3  11571  fsum3cvg3  11580  mertenslemi1  11719  ntrivcvgap0  11733  zproddc  11763  fprodseq  11767  fprodntrivap  11768  dvdsval2  11974  dvds0lem  11985  dvds1lem  11986  dvds2lem  11987  odd2np1lem  12056  odd2np1  12057  opeo  12081  omeo  12082  divalglemex  12106  bezoutlemnewy  12190  bezoutlemaz  12197  bezoutlembz  12198  bezoutlemsup  12203  nnwodc  12230  uzwodc  12231  ncoprmgcdne1b  12284  exprmfct  12333  reumodprminv  12449  modprm0  12450  nnnn0modprm0  12451  pythagtriplem19  12478  pcprmpw2  12529  pockthi  12554  infpnlem2  12556  ennnfonelemex  12658  ennnfonelemhom  12659  ennnfonelemrn  12663  ennnfonelemnn0  12666  ennnfonelemim  12668  exmidunben  12670  ctinfomlemom  12671  ctinfom  12672  ctinf  12674  ctiunctlemf  12682  ismgmid2  13084  mgmidsssn0  13088  ismndd  13141  isgrpd2  13225  isgrpd  13227  imasgrp2  13318  mhmmnd  13324  ghmgrp  13326  dvdsrmuld  13730  dvdsr01  13738  rhmdvdsr  13809  lspf  14023  lspval  14024  lssats2  14048  fiinbas  14393  topbas  14411  clsval  14455  neiint  14489  neipsm  14498  opnneissb  14499  opnssneib  14500  innei  14507  restbasg  14512  lmconst  14560  iscnp4  14562  cncnpi  14572  cnconst2  14577  cnptoprest  14583  cnpdis  14586  neitx  14612  txcnp  14615  blssps  14771  blss  14772  blssexps  14773  blssex  14774  ssblex  14775  blin2  14776  neibl  14835  metss2  14842  bdmopn  14848  metrest  14850  metcnp3  14855  tgioo  14898  tgqioo  14899  addcncntoplem  14905  cnopnap  14955  dedekindeulemuub  14961  suplociccreex  14968  dedekindicclemuub  14970  ivthinclemlm  14978  ivthinclemum  14979  ivthinclemlopn  14980  ivthinclemuopn  14982  ivthreinc  14989  elply2  15079  reeff1oleme  15116  sin0pilem2  15126  sgmnncl  15332  dvdsppwf1o  15333  perfect  15345  bj-nn0suc0  15704  bj-inf2vnlem1  15724  nninfsellemeq  15769  nninfomnilem  15773  qdencn  15784  trirec0  15801